awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
F : Type u_2
inst : Field F
P : RingPreordering F
⊢ P.support = ⊥

Tactic:
simpa [← Submodule.toAddSubgroup_inj] using supportAddSubgroup_eq_bot P

Premises used: RingPreordering.supportAddSubgroup_eq_bot, Submodule.toAddSubgroup_inj
-- 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
⊢ P.support.IsPrime

Tactic:
simpa using Ideal.isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P

Tactic:
⟨fun _ a b _ => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
refine_2 : ∀ (h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P), P.IsOrdering
⊢ P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P

Tactic:
refine ⟨fun _ a b _ => ?_, fun h => ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.IsOrdering
a b : R
h_1 : -(a * b) ∈ P
refine_1 : ∀ (this : ¬(a ∈ P ∨ b ∈ P)), False
⊢ a ∈ P ∨ b ∈ P

Tactic:
by_contra
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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)
⊢ -a ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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)
⊢ -b ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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)
⊢ a * b ∈ P

Tactic:
simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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)
⊢ a * b ∈ P

Tactic:
have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
⊢ a * b ∈ P.support

Tactic:
simp_all [mem_support]

Premises used: RingPreordering.mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
⊢ 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])
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : a * b ∈ P
this : a ∈ P.support ∨ b ∈ P.support
⊢ False

Tactic:
simp_all [mem_support]

Premises used: RingPreordering.mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ ∀ (a : R), a ∈ P ∨ -a ∈ P

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ HasMemOrNegMem P

Tactic:
have : HasMemOrNegMem P := ⟨by simp [h]⟩
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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

Tactic:
IsOrdering.mk' P (fun {x y} _ => ?_)

Premises used: RingPreordering.IsOrdering.mk'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
refine_2 : ∀ {x y : R}, x * y ∈ P.support → x ∈ P.support ∨ y ∈ P.support
⊢ P.IsOrdering

Tactic:
refine IsOrdering.mk' P (fun {x y} _ => ?_)

Premises used: RingPreordering.IsOrdering.mk'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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
refine_2 : ∀ (this : ¬(x ∈ P.support ∨ y ∈ P.support)), False
⊢ x ∈ P.support ∨ y ∈ P.support

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

Tactic:
have := h (-x) y
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
⊢ -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P

Tactic:
have := h (-x) (-y)
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
⊢ -(x * y) ∈ P → x ∈ P ∨ y ∈ P

Tactic:
have := h x y
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
⊢ -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P

Tactic:
have := h x (-y)
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
⊢ x ∈ P ∨ -x ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
refine_2 : x ∈ P → False
refine_2₁ : -x ∈ P → False
⊢ False

Tactic:
cases (by aesop : x ∈ P ∨ -x ∈ P)
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h_2 : x ∈ P
⊢ False

Tactic:
simp_all [mem_support]

Premises used: RingPreordering.mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Basic
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_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h_2 : -x ∈ P
⊢ False

Tactic:
simp_all [mem_support]

Premises used: RingPreordering.mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
p q : RingPreordering R
h :
  Eq.{u_1 + 1} (α := Set R) ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) p)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)
mk :
  ∀ (toSubsemiring : Subsemiring R) (mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier)
    (neg_one_notMem' : -1 ∉ toSubsemiring.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set R)
        ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
          { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
        ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)),
    { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
        RingPreordering R } =
      q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
q : RingPreordering R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)
mk :
  ∀ (toSubsemiring_1 : Subsemiring R) (mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier)
    (neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set R)
        ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
          { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
        ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
          { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
            neg_one_notMem' := neg_one_notMem'_1 })),
    { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
        RingPreordering R } =
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 }
⊢ { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    q

Tactic:
cases q
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
toSubsemiring_1 : Subsemiring R
mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier
neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 })
mk : toSubsemiring = toSubsemiring_1
⊢ { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1, neg_one_notMem' := neg_one_notMem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
toSubsemiring_1 : Subsemiring R
mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier
neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
toSubsemiring_1 : Subsemiring R
mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier
neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
exact SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
hx : IsSquare x
⊢ x ∈ P

Tactic:
RingPreordering.mem_of_isSquare' _ hx

Premises used: Set.Mem, RingPreordering.mem_of_isSquare'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
⊢ x * x ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
⊢ HPow.hPow (β := ℕ) x 2 ∈ P

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ -1 ∉ P

Tactic:
RingPreordering.neg_one_notMem' _

Premises used: Set.Mem, RingPreordering.neg_one_notMem'
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
A B : RingPreordering R
h : (↑A : Subsemiring R) = (↑B : Subsemiring R)
carrier : ∀ (x : R), x ∈ (↑A : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier
⊢ A = B

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
A B : RingPreordering R
h : (↑A : Subsemiring R) = (↑B : Subsemiring R)
x : R
carrier carrier₁ : x ∈ (↑B : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier
⊢ x ∈ (↑A : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P₁ P₂ : RingPreordering R
⊢ (↑P₁ : Subsemiring R) = (↑P₂ : Subsemiring R) ↔ P₁ = P₂

Tactic:
toSubsemiring_injective.eq_iff

Premises used: Function.Injective.eq_iff, RingPreordering.toSubsemiring_injective
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
⊢ x ∈ (↑P : Subsemiring R) ↔ x ∈ P

Tactic:
.rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem : -1 ∉ toSubsemiring.carrier
x : R
⊢ x ∈
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare, neg_one_notMem' := neg_one_notMem :
        RingPreordering R } ↔
    x ∈ toSubsemiring

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem : -1 ∉ toSubsemiring.carrier
⊢ (↑{ toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare, neg_one_notMem' := neg_one_notMem :
          RingPreordering R } :
      Set R) =
    (↑toSubsemiring : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
a b : R
ha : a ∈ S
hb : b ∈ S
⊢ a * b ∈ S

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
⊢ 1 ∈ S

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
a b : R
ha : a ∈ S
hb : b ∈ S
⊢ a + b ∈ S

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
⊢ 0 ∈ S

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
x : R
⊢ x ∈ P.copy S hS ↔ x ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
S : Set R
hS : S = (↑P : Set R)
⊢ (↑(P.copy S hS) : Set R) = S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ ∀ {a b : R},
    a ∈ (↑P : Set R) ∩ -(↑P : Set R) → b ∈ (↑P : Set R) ∩ -(↑P : Set R) → a + b ∈ (↑P : Set R) ∩ -(↑P : Set R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ 0 ∈ (↑P : Set R) ∩ -(↑P : Set R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ ∀ {x : R}, x ∈ (↑P : Set R) ∩ -(↑P : Set R) → -x ∈ (↑P : Set R) ∩ -(↑P : Set R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
x : R
⊢ x ∈ P.supportAddSubgroup ↔ x ∈ P ∧ -x ∈ P

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
⊢ (↑P.supportAddSubgroup : Set R) = (↑P : Set R) ∩ -(↑P : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : P.HasIdealSupport
⊢ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
simpa [mem_supportAddSubgroup] using P.smul_mem_support

Premises used: RingPreordering.mem_supportAddSubgroup, RingPreordering.HasIdealSupport.smul_mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
⊢ ∀ (x : R) {a : R} (ha : a ∈ P.supportAddSubgroup), x * a ∈ P.supportAddSubgroup

Tactic:
simpa [mem_supportAddSubgroup]

Premises used: RingPreordering.mem_supportAddSubgroup
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ (↑P : Set R)

Tactic:
simpa using mul_mem hx ha.1

Premises used: And.left, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ -(↑P : Set R)

Tactic:
simpa using mul_mem hx ha.2

Premises used: And.right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ (↑P : Set R)

Tactic:
simpa using mul_mem hx ha.2

Premises used: And.right, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ -(↑P : Set R)

Tactic:
simpa using mul_mem hx ha.1

Premises used: And.left, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ ∀ (c : R) {x : R}, x ∈ P.supportAddSubgroup.carrier → c • x ∈ P.supportAddSubgroup.carrier

Tactic:
simpa using smul_mem_support P

Premises used: RingPreordering.HasIdealSupport.smul_mem_support
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
x : R
⊢ x ∈ P.support ↔ x ∈ P ∧ -x ∈ P

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ (↑P.support : Set R) = (↑P : Set R) ∩ -(↑P : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Order.Ring.Ordering.Defs
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
inst_1 : P.HasIdealSupport
⊢ P.supportAddSubgroup = Submodule.toAddSubgroup P.support

Tactic:
rfl

Premises used: RingPreordering.supportAddSubgroup, rfl
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
⊢ HPow.hPow (β := ℕ) a 0 + (↑0 : R) * a ^ HSub.hSub (α := ℕ) 0 1 * b ≤ HPow.hPow (β := ℕ) (a + b) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
⊢ HPow.hPow (β := ℕ) a 1 + (↑1 : R) * a ^ HSub.hSub (α := ℕ) 1 1 * b ≤ HPow.hPow (β := ℕ) (a + b) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
⊢ HPow.hPow (β := ℕ) a 2 + (↑2 : R) * HPow.hPow (β := ℕ) a 1 * b + HPow.hPow (β := ℕ) b 2 = HPow.hPow (β := ℕ) (a + b) 2

Tactic:
simp [sq, add_mul, mul_add, two_mul, Hcomm.eq, add_assoc]

Premises used: add_mul, add_assoc, two_mul, sq, mul_add, Commute.eq
-- Module: Mathlib.Algebra.Order.Ring.Pow
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤
    HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
      a ^ (n + 1) * HPow.hPow (β := ℕ) b 2

Tactic:
apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]

Premises used: mul_nonneg, pow_nonneg, Nat.cast_nonneg, add_nonneg, zero_le_one