awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s : Finset β
hnonempty : s.Nonempty
l : β → α
⊢ f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun (i : β) ↦ f (l i)
have singleton : ∀ (i : β), f (∑ i ∈ {i}, l i) ≤ sup' {i} sorry fun (i : β) ↦ f (l i)
Tactic: induction hnonempty using Nonempty.cons_induction with
  | singleton i => simp
  | cons i s _ hs hind =>
    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
    rw [← le_sup'_iff hs]
    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
    · exact .inl h₁
    · exact .inr <| le_trans h₂ hind
Cleared hypotheses: hnonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : LinearOrder R
α : Type u_2
β : Type u_3
inst_1 : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s : Finset β
hnonempty : s.Nonempty
l : β → α
singleton : ∀ (i : β), f (∑ i ∈ {i}, l i) ≤ sup' {i} ⋯ fun (i : β) ↦ f (l i)
⊢ f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun (i : β) ↦ f (l i)
have cons : ∀ (i : β) (s : Finset β) (h : i ∉ s) (hs : s.Nonempty) (hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun (i : β) ↦ f (l i)),
  f (∑ i ∈ cons i s h, l i) ≤ (cons i s h).sup' sorry fun (i : β) ↦ f (l i)
Tactic: induction hnonempty using Nonempty.cons_induction with
  | singleton i => simp
  | cons i s _ hs hind =>
    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
    rw [← le_sup'_iff hs]
    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
    · exact .inl h₁
    · exact .inr <| le_trans h₂ hind
Cleared hypotheses: hnonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
have this : s.Nonempty
Tactic: have : s.Nonempty := by use k
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
have pos : ∀ (ha : k = a), Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
Tactic: by_cases ha : k = a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
pos :
  ∀ (ha : k = a), Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
have neg : ∀ (ha : ¬k = a), Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
Tactic: by_cases ha : k = a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
have pos : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (l a + ∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
Tactic: rw [sum_cons, ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (l a + ∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
have pos : LT.lt.{u_1} (α := R) ((f : (a : α) → R) (∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
Tactic: apply add_eq_left_of_lt nonarch
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s_1 : Finset β
l : β → α
a : β
s : Finset β
h : a ∉ s
hs : s.Nonempty
h_1 :
  ∀ {k : β} (hk : k ∈ s)
    (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
k : β
hk : k ∈ cons a s h
hmax : ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
ha : k = a
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) (∑ x ∈ s, l x) : R) ((f : (a : α) → R) (l a) : R)
have pos : LT.lt.{u_1} (α := R) (s.sup' hs fun (i : β) ↦ (f : (a : α) → R) (l i) : R) ((f : (a : α) → R) (l a) : R)
Tactic: grw [apply_sum_le_sup nonarch hs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
this : s.Nonempty
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
have singleton : ∀ (a : β) {k : β} (hk : Membership.mem (γ := Finset β) {a} k)
  (hmax :
    ∀ (j : β),
      Membership.mem (γ := Finset β) {a} j →
        j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
  Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ {a}, l i) : R) ((f : (a : α) → R) (l k) : R)
Tactic: induction this using Nonempty.cons_induction generalizing k with
  | singleton a => simp_all
  | cons a s _ hs _ =>
    by_cases ha : k = a
    · rw [sum_cons, ha]
      apply add_eq_left_of_lt nonarch
      grw [apply_sum_le_sup nonarch hs]
      grind [sup'_lt_iff]
    · grind [add_eq_right_of_lt nonarch]
Cleared hypotheses: k, hk, hmax, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
α : Type u_2
β : Type u_3
F : Type u_4
inst_2 : AddCommGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
nonarch : IsNonarchimedean.{u_1, u_2} (R := R) (α := α) (⇑f : (a : α) → R)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)
this : s.Nonempty
singleton :
  ∀ (a : β) {k : β} (hk : Membership.mem (γ := Finset β) {a} k)
    (hmax :
      ∀ (j : β),
        Membership.mem (γ := Finset β) {a} j →
          j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
    Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ {a}, l i) : R) ((f : (a : α) → R) (l k) : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)
have cons : ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
  (∀ {k : β} (hk : k ∈ s)
      (hmax : ∀ j ∈ s, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
      Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ s, l i) : R) ((f : (a : α) → R) (l k) : R)) →
    ∀ {k : β} (hk : k ∈ cons a s h)
      (hmax :
        ∀ j ∈ cons a s h, j ≠ k → LT.lt.{u_1} (α := R) ((f : (a : α) → R) (l j) : R) ((f : (a : α) → R) (l k) : R)),
      Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (∑ i ∈ cons a s h, l i) : R) ((f : (a : α) → R) (l k) : R)
Tactic: induction this using Nonempty.cons_induction generalizing k with
  | singleton a => simp_all
  | cons a s _ hs _ =>
    by_cases ha : k = a
    · rw [sum_cons, ha]
      apply add_eq_left_of_lt nonarch
      grw [apply_sum_le_sup nonarch hs]
      grind [sup'_lt_iff]
    · grind [add_eq_right_of_lt nonarch]
Cleared hypotheses: k, hk, hmax, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : CommRing α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a b : α
⊢ ∃ m < n + 1,
    (f : (a : α) → R) ((a + b) ^ n) ≤
      HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
have obtain : ∀ (m : ℕ) (hm_lt : (Finset.range (n + 1)).Nonempty → m ∈ Finset.range (n + 1))
  (hM :
    LE.le.{u_1} (α := R) ((f : (a : α) → R) (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
      ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)),
  ∃ m < n + 1,
    (f : (a : α) → R) ((a + b) ^ n) ≤
      HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
Tactic: obtain ⟨m, hm_lt, hM⟩ := finset_image_add hna
    (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : CommRing α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a b : α
m : ℕ
hm_lt : (Finset.range (n + 1)).Nonempty → m ∈ Finset.range (n + 1)
hM :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
    ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
⊢ ∃ m < n + 1,
    (f : (a : α) → R) ((a + b) ^ n) ≤
      HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
have hm_lt₁ : m < n + 1
Tactic: simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
    forall_true_left] at hm_lt
Cleared hypotheses: hm_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : CommRing α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a b : α
m : ℕ
hM :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
    ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
hm_lt : m < n + 1
⊢ ∃ m < n + 1,
    (f : (a : α) → R) ((a + b) ^ n) ≤
      HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
have refine : (f : (a : α) → R) ((a + b) ^ n) ≤
  HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
Tactic: refine ⟨m, hm_lt, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : CommRing α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a b : α
m : ℕ
hM :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
    ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
hm_lt : m < n + 1
⊢ (f : (a : α) → R) ((a + b) ^ n) ≤
    HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
have hM₁ : LE.le.{u_1} (α := R) ((f : (a : α) → R) ((a + b) ^ n) : R)
  ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
Tactic: simp only [← add_pow] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : CommRing α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM :
  LE.le.{u_1} (α := R) ((f : (a : α) → R) ((a + b) ^ n) : R)
    ((f : (a : α) → R) (a ^ m * b ^ (n - m) * (↑(n.choose m) : α)) : R)
⊢ (f : (a : α) → R) ((a + b) ^ n) ≤
    HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - m)) : R)
have hM₁ : LE.le.{u_1} (α := R) ((f : (a : α) → R) ((a + b) ^ n) : R)
  ((f : (a : α) → R) ((↑(n.choose m) : α) * (a ^ m * b ^ (n - m))) : R)
Tactic: rw [mul_comm] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
a : Rˣ
ha : (↑a : R) ∈ P
⊢ (↑a⁻¹ : R) ∈ P
have this : (↑a : R) * ((↑a⁻¹ : R) * (↑a⁻¹ : R)) ∈ P
Tactic: have : (a * (a⁻¹ * a⁻¹) : R) ∈ P := by aesop (config := { enableSimp := false })
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
⊢ a⁻¹ ∈ P
have mem : a * (a⁻¹ * a⁻¹) ∈ P
Tactic: have mem : a * (a⁻¹ * a⁻¹) ∈ P := by aesop
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
mem : a * (a⁻¹ * a⁻¹) ∈ P
⊢ a⁻¹ ∈ P
have mem₁ : 1 / a ∈ P
Tactic: field_simp at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
hx : IsSumSq x
⊢ x ∈ P
have zero : 0 ∈ P
Tactic: induction hx using IsSumSq.rec'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
hx : IsSumSq x
zero : 0 ∈ P
⊢ x ∈ P
have sq_add : ∀ {x s : R}, IsSquare x → IsSumSq s → s ∈ P → x + s ∈ P
Tactic: induction hx using IsSumSq.rec'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ P.support ≠ ⊤
have apply_fun : Ne.{u_1 + 1} (α := AddSubgroup R) (Submodule.toAddSubgroup P.support)
  (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule) ⊤)
Tactic: apply_fun Submodule.toAddSubgroup
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ x * a ∈ P
have rw : (∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P) → ∀ (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P), x * a ∈ P
Tactic: rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›
Cleared hypotheses: inst_1, x, a, h₁a, h₂a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ -(x * a) ∈ P
have rw : (∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P) → ∀ (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P), -(x * a) ∈ P
Tactic: rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›
Cleared hypotheses: inst_1, x, a, h₁a, h₂a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
⊢ P.HasIdealSupport
have rw : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
Tactic: rw [hasIdealSupport_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
x a : R
h_1 : a ∈ P
h_2 : -a ∈ P
⊢ x * a ∈ P ∧ -(x * a) ∈ P
have rcases : ∀ (half : R) (h2 : 2 * half = 1), x * a ∈ P ∧ -(x * a) ∈ P
Tactic: rcases h.exists_right_inv with ⟨half, h2⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
x a : R
h_1 : a ∈ P
h_2 : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ x * a ∈ P ∧ -(x * a) ∈ P
have rw : (HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a ∈ P ∧ -((HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a) ∈ P
Tactic: rw [show x = y ^ 2 - z ^ 2 by
    linear_combination (-x - x * half * 2) * h2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
x a : R
h_1 : a ∈ P
h_2 : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ (HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a ∈ P ∧
    -((HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a) ∈ P
have ring_nf : HPow.hPow (β := ℕ) y 2 * a - HPow.hPow (β := ℕ) z 2 * a ∈ P ∧
  -(HPow.hPow (β := ℕ) y 2 * a) + HPow.hPow (β := ℕ) z 2 * a ∈ P
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
⊢ x = 0
have by_contra : ∀ (this : ¬x = 0), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
⊢ False
have mem : -x * x⁻¹ ∈ P
Tactic: have mem : -x * x⁻¹ ∈ P := by aesop (erase simp neg_mul)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
mem : -x * x⁻¹ ∈ P
⊢ False
have mem₁ : -1 ∈ P
Tactic: field_simp at mem
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
⊢ P.supportAddSubgroup = ⊥
have h : ∀ (x : F), x ∈ P.supportAddSubgroup ↔ Membership.mem (γ := AddSubgroup F) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
have refine_1 : P.IsOrdering → ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
Tactic: refine ⟨fun _ a b _ => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
refine_1 : P.IsOrdering → ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
have refine_2 : ∀ (h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P), P.IsOrdering
Tactic: refine ⟨fun _ a b _ => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.IsOrdering
a b : R
h_1 : -(a * b) ∈ P
⊢ a ∈ P ∨ b ∈ P
have refine_1 : ∀ (this : ¬(a ∈ P ∨ b ∈ P)), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.IsOrdering
a b : R
h_1 : -(a * b) ∈ P
this : ¬(a ∈ P ∨ b ∈ P)
⊢ False
have this₁ : a * b ∈ P
Tactic: have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.IsOrdering
a b : R
h_1 : -(a * b) ∈ P
this_1 : ¬(a ∈ P ∨ b ∈ P)
this : a * b ∈ P
⊢ False
have this₁ : a ∈ P.support ∨ b ∈ P.support
Tactic: have : a ∈ P.support ∨ b ∈ P.support :=
      Ideal.IsPrime.mem_or_mem inferInstance (by simp_all [mem_support])
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ P.IsOrdering
have this : HasMemOrNegMem P
Tactic: have : HasMemOrNegMem P := ⟨by simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this : HasMemOrNegMem P
⊢ P.IsOrdering
have refine_2 : ∀ {x y : R}, x * y ∈ P.support → x ∈ P.support ∨ y ∈ P.support
Tactic: refine IsOrdering.mk' P (fun {x y} _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
⊢ x ∈ P.support ∨ y ∈ P.support
have refine_2 : ∀ (this : ¬(x ∈ P.support ∨ y ∈ P.support)), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this : ¬(x ∈ P.support ∨ y ∈ P.support)
⊢ False
have this₁ : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
Tactic: have := h (-x) y