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

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

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