Theorem: Lean4Axiomatic.AA.neqv_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) (_ : x₂ ≃ y)
State after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
⊢ False

State before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
⊢ False
Tactic:
have : x₁ ≃ y := Rel.trans ‹x₁ ≃ x₂› ‹x₂ ≃ y›
State after:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
this : x₁ ≃ y
⊢ False

State before:
α : Sort u
inst✝ : EqvOp α
x₁ x₂ y : α
x✝² : x₁ ≃ x₂
x✝¹ : x₁ ≄ y
x✝ : x₂ ≃ y
this : x₁ ≃ y
⊢ False
Tactic:
exact absurd ‹x₁ ≃ y› ‹x₁ ≄ y›
State after:
no goals