Theorem: Lean4Axiomatic.Logic.iff_subst_contra (Lean4Axiomatic/Logic.lean)

State before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
⊢ (p₁ ↔ p₂) → (f p₁ ↔ f p₂)
Tactic:
intro (Iff.intro (_ : p₁ → p₂) (_ : p₂ → p₁))
State after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂

State before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₂ → f p₁ := f_subst ‹p₁ → p₂›
State after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂

State before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₁ → f p₂ := f_subst ‹p₂ → p₁›
State after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₂ → f p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂

State before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₂ → f p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂
Tactic:
exact Iff.intro ‹f p₁ → f p₂› ‹f p₂ → f p₁›
State after:
no goals