Theorem: supp_zero_of_max_zero (UnitConjecture/FreeModule.lean)

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
hyp : maxNormSuccOnSupp norm crds s = 0
x : X
hm : x ∈ s
c : ¬crds x = 0
⊢ crds x = 0
Tactic:
let l := supp_below_max norm crds s x hm c
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
hyp : maxNormSuccOnSupp norm crds s = 0
x : X
hm : x ∈ s
c : ¬crds x = 0
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds s := supp_below_max norm crds s x hm c
⊢ crds x = 0

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
hyp : maxNormSuccOnSupp norm crds s = 0
x : X
hm : x ∈ s
c : ¬crds x = 0
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds s := supp_below_max norm crds s x hm c
⊢ crds x = 0
Tactic:
rw [hyp] at l
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
hyp : maxNormSuccOnSupp norm crds s = 0
x : X
hm : x ∈ s
c : ¬crds x = 0
l : norm x + 1 ≤ 0
⊢ crds x = 0

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
hyp : maxNormSuccOnSupp norm crds s = 0
x : X
hm : x ∈ s
c : ¬crds x = 0
l : norm x + 1 ≤ 0
⊢ crds x = 0
Tactic:
contradiction
State after:
no goals