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

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

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

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