Theorem: Lean4Axiomatic.AA.eqv_substL_iff (Lean4Axiomatic/AbstractAlgebra/Substitutive.lean)

State before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
⊢ x₁ ≃ x₂ → (x₁ ≃ y ↔ x₂ ≃ y)
Tactic:
intro (_ : x₁ ≃ x₂)
State after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ y ↔ x₂ ≃ y

State before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝ : x₁ ≃ x₂
⊢ x₁ ≃ y ↔ x₂ ≃ y
Tactic:
exact Iff.intro (eqv_substL ‹x₁ ≃ x₂›) (eqv_substL (Rel.symm ‹x₁ ≃ x₂›))
State after:
no goals