awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)

Tactic:
grind [add_eq_right_of_lt nonarch]

Premises used: IsNonarchimedean.add_eq_right_of_lt
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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 ∈ Finset.cons a s h)
        (hmax :
          ∀ j ∈ Finset.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 ∈ Finset.cons a s h, 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)

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]

Premises used: Finset.sum_cons, IsNonarchimedean.add_eq_left_of_lt, Finset.cons, Finset.sup'_lt_iff, IsNonarchimedean.add_eq_right_of_lt, Singleton.singleton
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
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)
⊢ ∃ 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))

Premises used: HMul.hMul, IsNonarchimedean.finset_image_add, HSub.hSub, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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

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

Premises used: forall_true_left, Finset.nonempty_range_iff, Finset.mem_range, ne_eq, Nat.succ_ne_zero, not_false_iff
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)

Tactic:
⟨m, hm_lt, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
refine :
  (f : (a : α) → R) ((a + b) ^ n) ≤
    HMul.hMul (α := R) (β := R) ((f : (a : α) → R) (a ^ m) : R) ((f : (a : α) → R) (b ^ (n - 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:
refine ⟨m, hm_lt, ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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
⊢ 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

Premises used: add_pow
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ 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

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) ((↑(n.choose m) : α) * (a ^ m * b ^ (n - 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)

Tactic:
le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

Premises used: IsNonarchimedean.nmul_le, le_trans, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) ((↑(n.choose m) : α) * (a ^ m * b ^ (n - 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)

Tactic:
exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

Premises used: IsNonarchimedean.nmul_le, le_trans, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Algebra.Order.Ring.Nat
Goal:
⊢ IsCompl (α := Set ℕ) {n : ℕ | Even n} {n : ℕ | Odd n}

Tactic:
simp only [← Set.compl_setOf, isCompl_compl, ← not_even_iff_odd]

Premises used: Nat.not_even_iff_odd, isCompl_compl, Set.compl_setOf
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P₁ P₂ : RingPreordering R
⊢ (↑P₁ : Subsemiring R) ≤ (↑P₂ : Subsemiring R) ↔ P₁ ≤ P₂

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P₁ P₂ : RingPreordering R
⊢ (↑P₁ : Subsemiring R) < (↑P₂ : Subsemiring R) ↔ P₁ < P₂

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
⊢ Monotone.{u_1, u_1} (α := RingPreordering R) toSubsemiring

Tactic:
fun _ _ => id

Premises used: Set.Mem, Monotone, id
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
⊢ StrictMono.{u_1, u_1} (α := RingPreordering R) toSubsemiring

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
a : Rˣ
ha : (↑a : R) ∈ P
⊢ (↑a : R) * ((↑a⁻¹ : R) * (↑a⁻¹ : R)) ∈ P

Tactic:
aesop (config := { enableSimp := false })
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
a : Rˣ
ha : (↑a : R) ∈ P
⊢ (↑a : R) * ((↑a⁻¹ : R) * (↑a⁻¹ : R)) ∈ P

Tactic:
have : (a * (a⁻¹ * a⁻¹) : R) ∈ P := by aesop (config := { enableSimp := false })
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
a : Rˣ
ha : (↑a : R) ∈ P
this : (↑a : R) * ((↑a⁻¹ : R) * (↑a⁻¹ : R)) ∈ P
⊢ (↑a⁻¹ : R) ∈ P

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
⊢ a * (a⁻¹ * a⁻¹) ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
⊢ a * (a⁻¹ * a⁻¹) ∈ P

Tactic:
have mem : a * (a⁻¹ * a⁻¹) ∈ P := by aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
mem : a * (a⁻¹ * a⁻¹) ∈ P
⊢ 1 / a ∈ P

Tactic:
field_simp at mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
a : F
ha : a ∈ P
mem : 1 / a ∈ P
⊢ a⁻¹ ∈ P

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
hx : IsSumSq x
zero : 0 ∈ P
sq_add : ∀ {x s : R}, IsSquare x → IsSumSq s → s ∈ P → x + s ∈ P
⊢ x ∈ P

Tactic:
induction hx using IsSumSq.rec'

Premises used: IsSumSq.rec'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
⊢ 0 ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x x_1 s : R
hx : IsSquare x_1
hs : IsSumSq s
h : s ∈ P
⊢ x_1 + s ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
P_1 : RingPreordering R_1
R_2 : Type u_2
inst_1 : CommRing R_2
P_2 : Set R_2
add_1 : Sort ?u.14782
mul_1 : add_1
sq_1 : Sort ?u.14788
neg_one_1 : sq_1
R : Type u_3
inst_2 : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x * y ∈ P

Tactic:
simpa using mul
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
P_1 : RingPreordering R_1
R_2 : Type u_2
inst_1 : CommRing R_2
P_2 : Set R_2
add_1 : Sort ?u.14782
mul_1 : add_1
sq_1 : Sort ?u.14788
neg_one_1 : sq_1
R : Type u_3
inst_2 : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 1 ∈ P

Tactic:
simpa using sq 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
P_1 : RingPreordering R_1
R_2 : Type u_2
inst_1 : CommRing R_2
P_2 : Set R_2
add_1 : Sort ?u.14782
mul_1 : add_1
sq_1 : Sort ?u.14788
neg_one_1 : sq_1
R : Type u_3
inst_2 : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x + y ∈ P

Tactic:
simpa using add
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
P_1 : RingPreordering R_1
R_2 : Type u_2
inst_1 : CommRing R_2
P_2 : Set R_2
add_1 : Sort ?u.14782
mul_1 : add_1
sq_1 : Sort ?u.14788
neg_one_1 : sq_1
R : Type u_3
inst_2 : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 0 ∈ P

Tactic:
simpa using sq 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_2
inst : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x : R
⊢ x ∈ mk' P add mul sq neg_one ↔ x ∈ P

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_2
inst : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ (↑(mk' P add mul sq neg_one) : Set R) = P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ 1 ∉ P.supportAddSubgroup

Tactic:
fun h => RingPreordering.neg_one_notMem P h.2

Premises used: And.right, RingPreordering.neg_one_notMem, Not
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ 1 ∉ P.support

Tactic:
simpa using one_notMem_supportAddSubgroup P

Premises used: RingPreordering.one_notMem_supportAddSubgroup
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.supportAddSubgroup = ⊤
⊢ 1 ∈ P.supportAddSubgroup

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
apply_fun :
  Ne.{u_1 + 1} (α := AddSubgroup R) (Submodule.toAddSubgroup P.support)
    (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule) ⊤)
⊢ P.support ≠ ⊤

Tactic:
apply_fun Submodule.toAddSubgroup

Premises used: Submodule.toAddSubgroup
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ Ne.{u_1 + 1} (α := AddSubgroup R) (Submodule.toAddSubgroup P.support)
    (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule) ⊤)

Tactic:
simpa using supportAddSubgroup_ne_top P

Premises used: RingPreordering.supportAddSubgroup_ne_top
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
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
⊢ x * a ∈ P

Tactic:
rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›

Premises used: RingPreordering.hasIdealSupport_iff, RingPreordering.HasIdealSupport
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ x * a ∈ P

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
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
⊢ -(x * a) ∈ P

Tactic:
rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›

Premises used: RingPreordering.hasIdealSupport_iff, RingPreordering.HasIdealSupport
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ -(x * a) ∈ P

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
rw : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
⊢ P.HasIdealSupport

Tactic:
rw [hasIdealSupport_iff]

Premises used: RingPreordering.hasIdealSupport_iff
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : IsUnit.{u_1} (M := R) 2
x a : R
_ : a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
⊢ a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
_
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
_ : -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
⊢ -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
_
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
rcases : ∀ (half : R) (h2 : 2 * half = 1), x * a ∈ P ∧ -(x * a) ∈ P
⊢ x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
rcases h.exists_right_inv with ⟨half, h2⟩

Premises used: IsUnit.exists_right_inv
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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 = HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2

Tactic:
linear_combination (-x - x * half * 2) * h2

Premises used: HMul.hMul, HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
rw :
  (HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a ∈ P ∧
    -((HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a) ∈ P
⊢ x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
rw [show x = y ^ 2 - z ^ 2 by
    linear_combination (-x - x * half * 2) * h2]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
ring_nf :
  HPow.hPow (β := ℕ) y 2 * a - HPow.hPow (β := ℕ) z 2 * a ∈ P ∧
    -(HPow.hPow (β := ℕ) y 2 * a) + HPow.hPow (β := ℕ) z 2 * a ∈ P
⊢ (HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a ∈ P ∧
    -((HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) z 2) * a) ∈ P

Tactic:
ring_nf
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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 * a - HPow.hPow (β := ℕ) z 2 * a ∈ P ∧
    -(HPow.hPow (β := ℕ) y 2 * a) + HPow.hPow (β := ℕ) z 2 * a ∈ P

Tactic:
aesop (add simp sub_eq_add_neg)

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : Fact (IsUnit.{u_1} (M := R) 2)
⊢ P.HasIdealSupport

Tactic:
hasIdealSupport_of_isUnit_two h.out

Premises used: RingPreordering.hasIdealSupport_of_isUnit_two, Fact.out
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
by_contra : ∀ (this : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
⊢ -x * x⁻¹ ∈ P

Tactic:
aesop (erase simp neg_mul)

Premises used: neg_mul
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
⊢ -x * x⁻¹ ∈ P

Tactic:
have mem : -x * x⁻¹ ∈ P := by aesop (erase simp neg_mul)
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
⊢ -1 ∈ P

Tactic:
field_simp at mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
mem : -1 ∈ P
⊢ False

Tactic:
RingPreordering.neg_one_notMem P mem

Premises used: RingPreordering.neg_one_notMem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
this : ¬x = 0
mem : -1 ∈ P
⊢ False

Tactic:
exact RingPreordering.neg_one_notMem P mem

Premises used: RingPreordering.neg_one_notMem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
h : ∀ (x : F), x ∈ P.supportAddSubgroup ↔ Membership.mem (γ := AddSubgroup F) ⊥ x
⊢ P.supportAddSubgroup = ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
x : F
⊢ x ∈ P.supportAddSubgroup ↔ Membership.mem (γ := AddSubgroup F) ⊥ x

Tactic:
aesop (add simp mem_supportAddSubgroup)

Premises used: RingPreordering.mem_supportAddSubgroup
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P_1 : RingPreordering R
F : Type u_2
inst_1 : Field F
P : RingPreordering F
⊢ ∀ (x : F) {a : F} (ha : a ∈ P.supportAddSubgroup), x * a ∈ P.supportAddSubgroup

Tactic:
simp [supportAddSubgroup_eq_bot]

Premises used: RingPreordering.supportAddSubgroup_eq_bot