Theorem: coeffInclusion_injective (UnitConjecture/FreeModule.lean)

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

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

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