internlm/Lean-Github huggingface dataset:
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
case inl p =>
    rw [p]
    rw [p] at h
    exact ⟨head, And.intro c rfl⟩
Proof state after:
no goals
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
rw [p]
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Tactic:
rw [p] at h
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : maxNormSuccOnSupp norm crds tail > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : maxNormSuccOnSupp norm crds tail > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Tactic:
exact  ih h
Proof state after:
no goals
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
rw [p]
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ norm head + 1 = norm x + 1
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ norm head + 1 = norm x + 1
Tactic:
rw [p] at h
Proof state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : norm head + 1 > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ norm head + 1 = norm x + 1
Theorem: max_in_support
Proof state before:
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : norm head + 1 > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ norm head + 1 = norm x + 1
Tactic:
exact ⟨head, And.intro c rfl⟩
Proof state after:
no goals
Theorem: supp_below_max
Proof 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₂
Proof 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
Theorem: supp_below_max
Proof 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₁
Proof 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✝)
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_below_max
Proof 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]
Proof 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
Theorem: supp_below_max
Proof 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₂]
Proof 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)
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_below_max
Proof 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]
Proof 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
Theorem: supp_below_max
Proof 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₂
Proof 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
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_below_max
Proof 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]
Proof 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)
Theorem: supp_below_max
Proof 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
Proof 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)
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_below_max
Proof 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]
Proof 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
Theorem: supp_below_max
Proof 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
Proof state after:
no goals
Theorem: supp_zero_of_max_zero
Proof 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
Proof 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
Theorem: supp_zero_of_max_zero
Proof 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
Proof 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
Theorem: supp_zero_of_max_zero
Proof 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
Proof state after:
no goals
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : normSucc norm s₁ = 0
⊢ normSucc norm s₁ ≤ normSucc norm s₂
Tactic:
rw [c]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : normSucc norm s₁ = 0
⊢ 0 ≤ normSucc norm s₂
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : normSucc norm s₁ = 0
⊢ 0 ≤ normSucc norm s₂
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬normSucc norm s₁ = 0
⊢ normSucc norm s₁ ≤ normSucc norm s₂
Tactic:
simp [FormalSum.normSucc]
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬normSucc norm s₁ = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬normSucc norm s₁ = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
simp [FormalSum.normSucc] at c
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
    by
    cases Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))
    contradiction
    assumption
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let l := max_in_support norm s₁.coords s₁.support c'
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
l : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)