Theorem: max_in_support (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
⊢ maxNormSuccOnSupp norm crds s > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1
Tactic:
intro 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
h : maxNormSuccOnSupp norm crds s > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1

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
h : maxNormSuccOnSupp norm crds s > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1
Tactic:
induction s with
| nil => 
  simp [maxNormSuccOnSupp] at h
| cons head tail ih => 
  exact if c : crds head =0 then
    by 
      simp [maxNormSuccOnSupp, c]
      simp [maxNormSuccOnSupp, c] at h
      exact  ih h
      
  else by    
      simp [maxNormSuccOnSupp, c]
      simp [maxNormSuccOnSupp, c] at h
      let sl := eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
      cases sl
      case inr p =>
          rw [p]
          rw [p] at h
          exact  ih h 
      case inl p =>
          rw [p]
          rw [p] at h
          exact ⟨head, And.intro c rfl⟩
State after:
no goals

State before:
case nil
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
h : maxNormSuccOnSupp norm crds [] > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds [] = norm x + 1
Tactic:
simp [maxNormSuccOnSupp] at h
State after:
no goals

State before:
case cons
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
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds (head :: tail) = norm x + 1
Tactic:
exact if c : crds head =0 then
  by 
    simp [maxNormSuccOnSupp, c]
    simp [maxNormSuccOnSupp, c] at h
    exact  ih h
    
else by    
    simp [maxNormSuccOnSupp, c]
    simp [maxNormSuccOnSupp, c] at h
    let sl := eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
    cases sl
    case inr p =>
        rw [p]
        rw [p] at h
        exact  ih h 
    case inl p =>
        rw [p]
        rw [p] at h
        exact ⟨head, And.intro c rfl⟩
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
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : crds head = 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds (head :: tail) = norm x + 1
Tactic:
simp [maxNormSuccOnSupp, 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
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : crds head = 0
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1

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
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : crds head = 0
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Tactic:
simp [maxNormSuccOnSupp, c] at 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
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
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1

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
⊢ ∃ x, ¬crds x = 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
Tactic:
exact  ih h
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
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : ¬crds head = 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds (head :: tail) = norm x + 1
Tactic:
simp [maxNormSuccOnSupp, 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
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : ¬crds head = 0
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1

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
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : ¬crds head = 0
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
simp [maxNormSuccOnSupp, c] at 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
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
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1

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
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
let sl := eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
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)
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1

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)
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
cases sl
State after:
case inl
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)
h✝ : 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

case inr
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)
h✝ : 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

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:
case inr p =>
    rw [p]
    rw [p] at h
    exact  ih h
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
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⟩
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
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]
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

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

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

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

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