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

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

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

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