Theorem: baseInclusion_injective (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
⊢ baseInclusion a₀ x₀ = baseInclusion a₀ x₁ → x₀ = x₁
Tactic:
intro hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : baseInclusion a₀ x₀ = baseInclusion a₀ x₁
⊢ x₀ = x₁

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : baseInclusion a₀ x₀ = baseInclusion a₀ x₁
⊢ x₀ = x₁
Tactic:
simp [baseInclusion] at hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : [(a₀, x₀)] ≈ [(a₀, x₁)]
⊢ x₀ = x₁

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : [(a₀, x₀)] ≈ [(a₀, x₁)]
⊢ x₀ = x₁
Tactic:
exact monom_elem_eq_of_coord_eq_nonzero a₀ non_zero x₀ x₁ hyp
State after:
no goals