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

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

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

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