Theorem: monom_elem_eq_of_coord_eq_nonzero (UnitConjecture/FreeModule.lean)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
⊢ coords [(a, x₀)] = coords [(a, x₁)] → x₀ = x₁
Tactic:
intro hyp
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ x₀ = x₁
Tactic:
have sup₀ : support [(a, x₀)] = [x₀] := by
  rfl
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ x₀ = x₁
Tactic:
have c₁ : coords [(a, x₁)] x₁ = a := by
  simp [coords, monomCoeff]
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
rw [← c₁] at non_zero
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : coords [(a, x₁)] x₁ ≠ 0
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : coords [(a, x₁)] x₁ ≠ 0
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
symm at non_zero
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₁)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₁)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
rw [← hyp] at non_zero
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
⊢ x₀ = x₁
Tactic:
let lem := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ ∈ support [(a, x₀)] := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ ∈ support [(a, x₀)] := nonzero_coord_in_support [(a, x₀)] x₁ non_zero
⊢ x₀ = x₁
Tactic:
simp [support] at lem
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₀ = x₁

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₀ = x₁
Tactic:
apply Eq.symm
State after:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₁ = x₀

State before:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
x₀ x₁ : X
non_zero : 0 ≠ coords [(a, x₀)] x₁
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
c₁ : coords [(a, x₁)] x₁ = a
lem : x₁ = x₀
⊢ x₁ = x₀
Tactic:
assumption
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
⊢ support [(a, x₀)] = [x₀]
Tactic:
rfl
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a : R
non_zero : a ≠ 0
x₀ x₁ : X
hyp : coords [(a, x₀)] = coords [(a, x₁)]
sup₀ : support [(a, x₀)] = [x₀]
⊢ coords [(a, x₁)] x₁ = a
Tactic:
simp [coords, monomCoeff]
State after:
no goals