Theorem: Lean4Axiomatic.AA.Prod.substR (Lean4Axiomatic/AbstractAlgebra/Substitutive.lean)

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

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ (y, x₁) ≃ (y, x₂)
Tactic:
apply eqv_defn.mpr
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ y ≃ y ∧ x₁ ≃ x₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ y ≃ y ∧ x₁ ≃ x₂
Tactic:
exact And.intro Rel.refl ‹x₁ ≃ x₂›
State after:
no goals