internlm/Lean-Github huggingface dataset:
Theorem: baseInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
⊢ baseInclusion a₀ x₀ = baseInclusion a₀ x₁ → x₀ = x₁
Tactic:
intro hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : baseInclusion a₀ x₀ = baseInclusion a₀ x₁
⊢ x₀ = x₁
Theorem: baseInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : baseInclusion a₀ x₀ = baseInclusion a₀ x₁
⊢ x₀ = x₁
Tactic:
simp [baseInclusion] at hyp
Proof state after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : [(a₀, x₀)] ≈ [(a₀, x₁)]
⊢ x₀ = x₁
Theorem: baseInclusion_injective
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a₀ : R
non_zero : a₀ ≠ 0
x₀ x₁ : X
hyp : [(a₀, x₀)] ≈ [(a₀, x₁)]
⊢ x₀ = x₁
Tactic:
exact monom_elem_eq_of_coord_eq_nonzero a₀ non_zero x₀ x₁ hyp
Proof state after:
no goals
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
⊢ a ≤ max a b
Tactic:
exact if c:a ≤ b 
      then by
          unfold max
          unfold Nat.instMaxNat
          unfold maxOfLe
          simp [if_pos c]
          assumption
      else by
          unfold max
          unfold Nat.instMaxNat
          unfold maxOfLe
          simp [if_neg c]
Proof state after:
no goals
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ max a b
Tactic:
unfold max
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ Nat.instMaxNat.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ maxOfLe.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_pos c]
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ b
Tactic:
assumption
Proof state after:
no goals
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ max a b
Tactic:
unfold max
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ Nat.instMaxNat.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ maxOfLe.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Theorem: fst_le_max
Proof state before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ a ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_neg c]
Proof state after:
no goals
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
⊢ b ≤ max a b
Tactic:
exact if c: a ≤ b
then by
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe 
  simp [if_pos c]
else by 
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe
  simp [if_neg c]
  apply Nat.le_of_lt
  let c' := Nat.gt_of_not_le c
  assumption
Proof state after:
no goals
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ max a b
Tactic:
unfold max
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ maxOfLe.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_pos c]
Proof state after:
no goals
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ max a b
Tactic:
unfold max
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ maxOfLe.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_neg c]
Proof state after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ a
Theorem: snd_le_max
Proof state before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ a
Tactic:
apply Nat.le_of_lt
Proof state after:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b < a
Theorem: snd_le_max
Proof state before:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b < a
Tactic:
let c' := Nat.gt_of_not_le c
Proof state after:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
c' : a > b := Nat.gt_of_not_le c
⊢ b < a
Theorem: snd_le_max
Proof state before:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
c' : a > b := Nat.gt_of_not_le c
⊢ b < a
Tactic:
assumption
Proof state after:
no goals
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
⊢ max a b = a ∨ max a b = b
Tactic:
exact if c: a ≤ b 
  then by
    unfold max
    unfold Nat.instMaxNat
    unfold maxOfLe
    simp [if_pos c]
  else by
    unfold max
    unfold Nat.instMaxNat
    unfold maxOfLe
    simp [if_neg c]
Proof state after:
no goals
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ max a b = a ∨ max a b = b
Tactic:
unfold max
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ Nat.instMaxNat.1 a b = a ∨ Nat.instMaxNat.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ Nat.instMaxNat.1 a b = a ∨ Nat.instMaxNat.1 a b = b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ maxOfLe.1 a b = a ∨ maxOfLe.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ maxOfLe.1 a b = a ∨ maxOfLe.1 a b = b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ { max := fun x y => if x ≤ y then y else x }.1 a b = a ∨ { max := fun x y => if x ≤ y then y else x }.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ { max := fun x y => if x ≤ y then y else x }.1 a b = a ∨ { max := fun x y => if x ≤ y then y else x }.1 a b = b
Tactic:
simp [if_pos c]
Proof state after:
no goals
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ max a b = a ∨ max a b = b
Tactic:
unfold max
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ Nat.instMaxNat.1 a b = a ∨ Nat.instMaxNat.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ Nat.instMaxNat.1 a b = a ∨ Nat.instMaxNat.1 a b = b
Tactic:
unfold Nat.instMaxNat
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ maxOfLe.1 a b = a ∨ maxOfLe.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ maxOfLe.1 a b = a ∨ maxOfLe.1 a b = b
Tactic:
unfold maxOfLe
Proof state after:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ { max := fun x y => if x ≤ y then y else x }.1 a b = a ∨ { max := fun x y => if x ≤ y then y else x }.1 a b = b
Theorem: eq_fst_or_snd_of_max
Proof state before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ { max := fun x y => if x ≤ y then y else x }.1 a b = a ∨ { max := fun x y => if x ≤ y then y else x }.1 a b = b
Tactic:
simp [if_neg c]
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
s : List X
⊢ maxNormSuccOnSupp norm crds s > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1
Tactic:
intro 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
h : maxNormSuccOnSupp norm crds s > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = 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
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⟩
Proof state after:
no goals
Theorem: max_in_support
Proof 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
Proof state after:
no goals
Theorem: max_in_support
Proof 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⟩
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
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]
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
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
c : crds head = 0
⊢ ∃ 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
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
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
⊢ ∃ 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
⊢ ∃ 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
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]
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
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
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
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
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
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (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
⊢ ∃ 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)
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)
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (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)
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm x + 1
Tactic:
cases sl
Proof 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
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:
case inr p =>
    rw [p]
    rw [p] at h
    exact  ih h
Proof state after:
no goals