internlm/Lean-Github huggingface dataset:
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₁))))
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₂)
Tactic:
let ⟨x₀, p⟩:= l
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
⊢ 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₁))))
l : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let nonzr' := p.left
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₁ x₀ ≠ 0 := p.left
⊢ 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₁))))
l : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₁ x₀ ≠ 0 := p.left
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let l := congrFun eql x₀
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₁ x₀ ≠ 0 := p.left
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
⊢ 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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₁ x₀ ≠ 0 := p.left
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
rw [l] at nonzr'
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
⊢ 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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let nonzr : 0 ≠ s₂.coords x₀ := by
  intro hyp
  let l' := Eq.symm hyp
  contradiction
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
⊢ 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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
let in_supp := nonzero_coord_in_support s₂ x₀ nonzr
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
in_supp : x₀ ∈ support s₂ := nonzero_coord_in_support s₂ x₀ nonzr
⊢ 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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
in_supp : x₀ ∈ support s₂ := nonzero_coord_in_support s₂ x₀ nonzr
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
rw [p.right]
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
in_supp : x₀ ∈ support s₂ := nonzero_coord_in_support s₂ x₀ nonzr
⊢ norm x₀ + 1 ≤ 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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
nonzr : 0 ≠ coords s₂ x₀ :=
  fun hyp =>
    let l' := hyp.symm;
    absurd l' nonzr'
in_supp : x₀ ∈ support s₂ := nonzero_coord_in_support s₂ x₀ nonzr
⊢ norm x₀ + 1 ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
Tactic:
apply supp_below_max norm s₂.coords s₂.support x₀ in_supp nonzr'
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 : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
Tactic:
cases Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))
Proof state after:
case inl
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0

case inr
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
Theorem: normsucc_le
Proof state before:
case inl
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0

case inr
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
Tactic:
contradiction
Proof state after:
case inr
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
Theorem: normsucc_le
Proof state before:
case inr
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
Tactic:
assumption
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 : ¬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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
⊢ 0 ≠ coords s₂ x₀
Tactic:
intro hyp
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
hyp : 0 = coords s₂ x₀
⊢ False
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₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
hyp : 0 = coords s₂ x₀
⊢ False
Tactic:
let l' := Eq.symm hyp
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'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
hyp : 0 = coords s₂ x₀
l' : coords s₂ x₀ = 0 := hyp.symm
⊢ False