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

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

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