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

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

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