Theorem: Lean4Axiomatic.Relation.Equivalence.iff_subst_eqv (Lean4Axiomatic/Relation/Equivalence/Core.lean)

State before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
⊢ x₁ ≃ x₂ → (P x₁ ↔ P x₂)
Tactic:
intro (_ : x₁ ≃ x₂)
State after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
⊢ P x₁ ↔ P x₂

State before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
⊢ P x₁ ↔ P x₂
Tactic:
have : P x₁ → P x₂ := P_subst ‹x₁ ≃ x₂›
State after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this : P x₁ → P x₂
⊢ P x₁ ↔ P x₂

State before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this : P x₁ → P x₂
⊢ P x₁ ↔ P x₂
Tactic:
have : P x₂ → P x₁ := P_subst (symm ‹x₁ ≃ x₂›)
State after:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this✝ : P x₁ → P x₂
this : P x₂ → P x₁
⊢ P x₁ ↔ P x₂

State before:
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this✝ : P x₁ → P x₂
this : P x₂ → P x₁
⊢ P x₁ ↔ P x₂
Tactic:
exact Iff.intro ‹P x₁ → P x₂› ‹P x₂ → P x₁›
State after:
no goals