iff_intro / iff_rintro

Build an Iff from its two directions, folding the introduction of each side's hypothesis into the split — constructor followed by two intros, in one tactic.

def CustomPrelude.Tactic.tacticIff_intro___ : Lean.ParserDescr

Split an Iff goal and introduce one hypothesis on each side.

Equations

• One or more equations did not get rendered due to their size.

def CustomPrelude.Tactic.tacticIff_rintro___ : Lean.ParserDescr

Split an Iff goal and rintro one pattern on each side.

Equations

• One or more equations did not get rendered due to their size.