Theorem: normsucc_le (UnitConjecture/FreeModule.lean)

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]
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₂

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
State after:
no goals

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]
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₂)

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
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₂)

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
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₂)

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'
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₂)

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
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₂)

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
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₂)

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₀
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₂)

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'
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₂)

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
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₂)

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
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₂)

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]
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₂)

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'
State after:
no goals

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₁))
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

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
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

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
State after:
no goals

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
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

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
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

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₀
l' : coords s₂ x₀ = 0 := hyp.symm
⊢ False
Tactic:
contradiction
State after:
no goals