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

State before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
⊢ f x₁ ≄ f x₂ → x₁ ≄ x₂
Tactic:
intro (_ : f x₁ ≃ f x₂ → False) (_ : x₁ ≃ x₂)
State after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ False

State before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ False
Tactic:
apply ‹f x₁ ≃ f x₂ → False›
State after:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ f x₁ ≃ f x₂

State before:
α : Sort u
β : Sort v
inst✝² : EqvOp α
inst✝¹ : EqvOp β
f : α → β
x₁ x₂ : α
inst✝ : Substitutive₁ f (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x✝¹ : f x₁ ≃ f x₂ → False
x✝ : x₁ ≃ x₂
⊢ f x₁ ≃ f x₂
Tactic:
exact subst₁ ‹x₁ ≃ x₂›
State after:
no goals