Theorem: supp_below_max (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
⊢ ∀ (x : X), x ∈ s → crds x ≠ 0 → norm x + 1 ≤ maxNormSuccOnSupp norm crds s
Tactic:
intro x h₁ h₂
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
x : X
h₁ : x ∈ s
h₂ : crds x ≠ 0
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds s

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
x : X
h₁ : x ∈ s
h₂ : crds x ≠ 0
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds s
Tactic:
cases h₁
State after:
case head
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as✝ : List X
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (x :: as✝)

case tail
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
b✝ : X
as✝ : List X
a✝ : List.Mem x as✝
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (b✝ :: as✝)

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (x :: as)
Tactic:
case head as => 
  rw [maxNormSuccOnSupp]
  simp [h₂]
  apply fst_le_max
State after:
no goals

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (a :: as)
Tactic:
case tail a as th =>
  rw [maxNormSuccOnSupp]
  let l := supp_below_max norm crds as  x  th h₂ 
  exact if c:crds a ≠ 0 then
    by
    simp [c]
    apply Nat.le_trans l 
    apply snd_le_max
  else
    by 
    simp [c]
    exact l
State after:
no goals

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (x :: as)
Tactic:
rw [maxNormSuccOnSupp]
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ if crds x ≠ 0 then max (norm x + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ if crds x ≠ 0 then max (norm x + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as
Tactic:
simp [h₂]
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ max (norm x + 1) (maxNormSuccOnSupp norm crds as)

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
as : List X
⊢ norm x + 1 ≤ max (norm x + 1) (maxNormSuccOnSupp norm crds as)
Tactic:
apply fst_le_max
State after:
no goals

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (a :: as)
Tactic:
rw [maxNormSuccOnSupp]
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as
Tactic:
let l := supp_below_max norm crds as  x  th h₂
State after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as
Tactic:
exact if c:crds a ≠ 0 then
  by
  simp [c]
  apply Nat.le_trans l 
  apply snd_le_max
else
  by 
  simp [c]
  exact l
State after:
no goals

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : crds a ≠ 0
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as
Tactic:
simp [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
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : crds a ≠ 0
⊢ norm x + 1 ≤ max (norm a + 1) (maxNormSuccOnSupp norm crds as)

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : crds a ≠ 0
⊢ norm x + 1 ≤ max (norm a + 1) (maxNormSuccOnSupp norm crds as)
Tactic:
apply Nat.le_trans 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
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : crds a ≠ 0
⊢ maxNormSuccOnSupp norm crds as ≤ max (norm a + 1) (maxNormSuccOnSupp norm crds as)

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : crds a ≠ 0
⊢ maxNormSuccOnSupp norm crds as ≤ max (norm a + 1) (maxNormSuccOnSupp norm crds as)
Tactic:
apply snd_le_max
State after:
no goals

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : ¬crds a ≠ 0
⊢ norm x + 1 ≤ if crds a ≠ 0 then max (norm a + 1) (maxNormSuccOnSupp norm crds as) else maxNormSuccOnSupp norm crds as
Tactic:
simp [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
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : ¬crds a ≠ 0
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds as

State before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
l : norm x + 1 ≤ maxNormSuccOnSupp norm crds as := supp_below_max norm crds as x th h₂
c : ¬crds a ≠ 0
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds as
Tactic:
exact l
State after:
no goals