Theorem: nonzero_coord_in_support (UnitConjecture/FreeModule.lean)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
⊢ x ∈ support []
Tactic:
have d : coords [] x = (0 : R) := by
  rfl
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
d : coords [] x = 0
⊢ x ∈ support []

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
d : coords [] x = 0
⊢ x ∈ support []
Tactic:
rw [d] at hyp
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ 0
d : coords [] x = 0
⊢ x ∈ support []

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ 0
d : coords [] x = 0
⊢ x ∈ support []
Tactic:
contradiction
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
x : X
hyp : 0 ≠ coords [] x
⊢ coords [] x = 0
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
s : FormalSum R X
h : R × X
t : List (R × X)
⊢ ∀ (x : X), 0 ≠ coords (h :: t) x → x ∈ support (h :: t)
Tactic:
intro x hyp
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
hyp : 0 ≠ coords (h :: t) x
⊢ x ∈ support (h :: t)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
hyp : 0 ≠ coords (h :: t) x
⊢ x ∈ support (h :: t)
Tactic:
let (a₀, x₀) := h
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ x ∈ support ((a₀, x₀) :: t)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ x ∈ support ((a₀, x₀) :: t)
Tactic:
have d : support ((a₀, x₀) :: t) = x₀ :: (support t) := by
  rfl
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ support ((a₀, x₀) :: t)

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ support ((a₀, x₀) :: t)
Tactic:
rw [d]
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ x₀ :: support t

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
⊢ x ∈ x₀ :: support t
Tactic:
match p : x₀ == x with
| true =>
  have eqn : x₀ = x := of_decide_eq_true p
  rw [eqn]
  apply List.mem_of_elem_eq_true
  simp [List.elem]
| false =>
  rw [coords, monomCoeff, p, zero_add] at hyp
  let step := nonzero_coord_in_support t x hyp
  apply List.mem_of_elem_eq_true
  simp [List.elem]
  have p' : (x == x₀) = false := by
    have eqn := of_decide_eq_false p
    have eqn' : ¬(x = x₀) := by
      intro contra
      let contra' := Eq.symm contra
      contradiction
    exact decide_eq_false eqn'
  rw [p']
  apply List.elem_eq_true_of_mem
  exact step
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
⊢ support ((a₀, x₀) :: t) = x₀ :: support t
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
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
⊢ x ∈ x₀ :: support t
Tactic:
have eqn : x₀ = x := of_decide_eq_true p
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x₀ :: support t

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x₀ :: support t
Tactic:
rw [eqn]
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x :: support t

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ x ∈ x :: support t
Tactic:
apply List.mem_of_elem_eq_true
State after:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ List.elem x (x :: support t) = true

State before:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = true
eqn : x₀ = x
⊢ List.elem x (x :: support t) = true
Tactic:
simp [List.elem]
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords ((a₀, x₀) :: t) x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support t
Tactic:
rw [coords, monomCoeff, p, zero_add] at hyp
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support t

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
⊢ x ∈ x₀ :: support t
Tactic:
let step := nonzero_coord_in_support t x hyp
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ x ∈ x₀ :: support t

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ x ∈ x₀ :: support t
Tactic:
apply List.mem_of_elem_eq_true
State after:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ List.elem x (x₀ :: support t) = true

State before:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ List.elem x (x₀ :: support t) = true
Tactic:
simp [List.elem]
State after:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true

State before:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
have p' : (x == x₀) = false := by
  have eqn := of_decide_eq_false p
  have eqn' : ¬(x = x₀) := by
    intro contra
    let contra' := Eq.symm contra
    contradiction
  exact decide_eq_false eqn'
State after:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true

State before:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match x == x₀ with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
rw [p']
State after:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match false with
    | true => true
    | false => List.elem x (support t)) =
    true

State before:
case a
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ (match false with
    | true => true
    | false => List.elem x (support t)) =
    true
Tactic:
apply List.elem_eq_true_of_mem
State after:
case a.h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ x ∈ support t

State before:
case a.h
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
p' : (x == x₀) = false
⊢ x ∈ support t
Tactic:
exact step
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
⊢ (x == x₀) = false
Tactic:
have eqn := of_decide_eq_false p
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ (x == x₀) = false

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ (x == x₀) = false
Tactic:
have eqn' : ¬(x = x₀) := by
  intro contra
  let contra' := Eq.symm contra
  contradiction
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
eqn' : ¬x = x₀
⊢ (x == x₀) = false

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
eqn' : ¬x = x₀
⊢ (x == x₀) = false
Tactic:
exact decide_eq_false eqn'
State after:
no goals

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
⊢ ¬x = x₀
Tactic:
intro contra
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
⊢ False

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
⊢ False
Tactic:
let contra' := Eq.symm contra
State after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
contra' : x₀ = x := contra.symm
⊢ False

State before:
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
s : FormalSum R X
h : R × X
t : List (R × X)
x : X
a₀ : R
x₀ : X
hyp : 0 ≠ coords t x
d : support ((a₀, x₀) :: t) = x₀ :: support t
p : (x₀ == x) = false
step : x ∈ support t := nonzero_coord_in_support t x hyp
eqn : ¬x₀ = x
contra : x = x₀
contra' : x₀ = x := contra.symm
⊢ False
Tactic:
contradiction
State after:
no goals