awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Eq.{u_2 + 1} (α := Subsemiring R) (Subsemiring.unop ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
⊢ S.unop = ⊤ ↔ S = ⊤

Tactic:
unop_injective.eq_iff' unop_top

Premises used: Function.Injective.eq_iff', Subsemiring.unop_injective, Subsemiring.unop_top
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring R
⊢ (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Tactic:
opEquiv.map_sup _ _

Premises used: Set.Mem, setOf, OrderIso.map_sup, Subsemiring.op, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring Rᵐᵒᵖ
⊢ (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Tactic:
opEquiv.symm.map_sup _ _

Premises used: Set.Mem, setOf, OrderIso.symm, OrderIso.map_sup, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring R
⊢ (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, setOf, Set.inter, Set.preimage, Subsemiring.op, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring Rᵐᵒᵖ
⊢ (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Set (Subsemiring R)
⊢ (sSup S).op = sSup (Subsemiring.unop ⁻¹' S)

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, Subsemiring.op, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Set (Subsemiring Rᵐᵒᵖ)
⊢ (sSup S).unop = sSup (Subsemiring.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sSup_eq_sSup_symm_preimage, OrderIso.symm, Subsemiring.op, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Set (Subsemiring R)
⊢ (sInf S).op = sInf (Subsemiring.unop ⁻¹' S)

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, Subsemiring.op, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Set (Subsemiring Rᵐᵒᵖ)
⊢ (sInf S).unop = sInf (Subsemiring.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, OrderIso.symm, Subsemiring.op, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : ι → Subsemiring R
⊢ (iSup S).op = ⨆ (i : ι), (S i).op

Tactic:
opEquiv.map_iSup _

Premises used: OrderIso.map_iSup, Subsemiring.op, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : ι → Subsemiring Rᵐᵒᵖ
⊢ (iSup S).unop = ⨆ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iSup _

Premises used: OrderIso.map_iSup, OrderIso.symm, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : ι → Subsemiring R
⊢ (iInf S).op = ⨅ (i : ι), (S i).op

Tactic:
opEquiv.map_iInf _

Premises used: OrderIso.map_iInf, Subsemiring.op, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : ι → Subsemiring Rᵐᵒᵖ
⊢ (iInf S).unop = ⨅ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iInf _

Premises used: OrderIso.map_iInf, OrderIso.symm, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set R
simp_rw :
  Eq.{u_2 + 1} (α := Subsemiring Rᵐᵒᵖ) (sInf {a : Subsemiring Rᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ)})
    (sInf {S : Subsemiring Rᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Rᵐᵒᵖ)})
⊢ Eq (α := Subsemiring Rᵐᵒᵖ) (Subsemiring.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]

Premises used: Subsemiring.closure, Subsemiring.op_sInf, Set.preimage_setOf_eq, Subsemiring.coe_unop
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set R
e_a : ∀ (a : Subsemiring Rᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)
⊢ Eq.{u_2 + 1} (α := Subsemiring Rᵐᵒᵖ) (sInf {a : Subsemiring Rᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ)})
    (sInf {S : Subsemiring Rᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Rᵐᵒᵖ)})

Tactic:
congr with a
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set R
a : Subsemiring Rᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.Subset, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set R
a : Subsemiring Rᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)

Tactic:
exact MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, MulOpposite.unop_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set Rᵐᵒᵖ
rw : Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
⊢ Eq (α := Subsemiring R) (Subsemiring.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))

Tactic:
rw [← op_inj, op_unop, op_closure]

Premises used: Subsemiring.op_closure, Subsemiring.op_inj, Subsemiring.op_unop
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set Rᵐᵒᵖ
simp_rw :
  Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
simp_rw₁ : Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ x) ⁻¹' s))
⊢ Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Premises used: Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id'
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
S : Type u_2
inst : SetLike S R
s : S
inst_1 : Semiring R
inst_2 : PartialOrder R
inst_3 : IsOrderedRing R
inst_4 : SubsemiringClass S R
⊢ IsOrderedRing.{u_1} ↥s

Tactic:
Function.Injective.isOrderedRing Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl

Premises used: Iff.rfl, Function.Injective.isOrderedRing, Subtype.val, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
S : Type u_2
inst : SetLike S R
s : S
inst_1 : Semiring R
inst_2 : PartialOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : SubsemiringClass S R
⊢ IsStrictOrderedRing.{u_1} ↥s

Tactic:
Function.Injective.isStrictOrderedRing Subtype.val
    rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) .rfl .rfl

Premises used: Iff.rfl, Function.Injective.isStrictOrderedRing, Subtype.val, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Subsemiring R
⊢ IsOrderedRing.{u_1} ↥s

Tactic:
SubsemiringClass.toIsOrderedRing _

Premises used: Set.Mem, SubsemiringClass.toIsOrderedRing
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
s : Subsemiring R
⊢ IsStrictOrderedRing.{u_1} ↥s

Tactic:
SubsemiringClass.toIsStrictOrderedRing _

Premises used: Set.Mem, SubsemiringClass.toIsStrictOrderedRing
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
⊢ Membership.mem (γ := Subsemiring R) (nonneg R) x ↔ 0 ≤ x

Tactic:
.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
⊢ Eq (α := AddSubmonoid R) (toAddSubmonoid (nonneg R)) (AddSubmonoid.nonneg R)

Tactic:
rfl

Premises used: Set.Ici, setOf, AddSubmonoid.nonneg, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Subsemiring R
⊢ a • S = map (MulSemiringAction.toRingHom M R a) S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
S : Subsemiring R
⊢ (↑(m • S) : Set R) = m • (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
S : Subsemiring R
⊢ (m • S).toAddSubmonoid = m • S.toAddSubmonoid

Tactic:
rfl

Premises used: AddMonoid.End.instFunLike._aux_1, Set.Mem, setOf, AddSubmonoid.map, Set.image, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
r : R
S : Subsemiring R
⊢ r ∈ S → m • r ∈ m • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ m • (S : Set R))

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
⊢ CovariantClass M (Subsemiring R) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ => image_mono⟩

Premises used: CovariantClass.mk, Set.image_mono
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
r : R
S : Subsemiring R
⊢ r ∈ m • S ↔ ∃ s ∈ S, m • s = r

Tactic:
(Set.mem_smul_set : r ∈ m • (S : Set R) ↔ _)

Premises used: Set.Mem, Set.mem_smul_set
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
⊢ HSMul.hSMul (β := Subsemiring R) a ⊥ = ⊥

Tactic:
map_bot _

Premises used: Subsemiring.map_bot
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Subsemiring R
⊢ a • (S ⊔ T) = a • S ⊔ a • T

Tactic:
map_sup _ _ _

Premises used: Subsemiring.map_sup, Set.Mem, setOf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
s : Set R
⊢ HSMul.hSMul (β := Subsemiring R) a (closure s) = closure (a • s)

Tactic:
RingHom.map_closureS _ _

Premises used: RingHom.map_closureS
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Monoid M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
inst_3 : MulSemiringAction.{u_1, u_2} Mᵐᵒᵖ R
inst_4 : IsCentralScalar M R
⊢ IsCentralScalar.{u_1, u_2} M (Subsemiring R)

Tactic:
⟨fun _a S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩

Premises used: RingHom.ext, congr_arg, IsCentralScalar.mk, Subsemiring.map, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Subsemiring R
x : R
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Subsemiring R
x : R
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S : Subsemiring R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Subsemiring R
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Subsemiring R
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : Group M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
S T : Subsemiring R
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subsemiring R
x : R
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff₀ ha (S : Set R) x

Premises used: Set.Mem, Set.smul_mem_smul_set_iff₀, SetLike.coe
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subsemiring R
x : R
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem₀ ha (S : Set R) x

Premises used: Set.Mem, SetLike.coe, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S : Subsemiring R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff₀ ha (S : Set R) x

Premises used: Set.mem_inv_smul_set_iff₀, Set.Mem, SetLike.coe
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subsemiring R
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff₀ ha

Premises used: Set.smul_set_subset_smul_set_iff₀, Set.Mem, Set.Subset
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subsemiring R
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff₀
-- Module: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Goal:
M : Type u_1
R : Type u_2
inst : GroupWithZero M
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
a : M
ha : a ≠ 0
S T : Subsemiring R
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff₀ ha

Premises used: Set.Mem, Set.Subset, Set.subset_smul_set_iff₀
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
inst_2 : Zero R
motive : (s : R) → (h : IsSumSq s) → Prop
zero : motive 0 ⋯
x s : R
hx : IsSquare x
hs : IsSumSq s
rcases : ∀ (w : R), IsSumSq (w * w + s)
⊢ IsSumSq (x + s)

Tactic:
rcases hx with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
inst_2 : Zero R
motive : (s : R) → (h : IsSumSq s) → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w : R
⊢ IsSumSq (w * w + s)

Tactic:
sq_add _ hs

Premises used: IsSumSq.sq_add
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
inst_2 : Zero R
motive : (s : R) → (h : IsSumSq s) → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w : R
⊢ IsSumSq (w * w + s)

Tactic:
exact sq_add _ hs

Premises used: IsSumSq.sq_add
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
inst_2 : Zero R
motive : (s : R) → (h : IsSumSq s) → Prop
zero : motive 0 ⋯
sq_add : ∀ {x s : R} (hx : IsSquare x) (hs : IsSumSq s), motive s hs → motive (x + s) ⋯
s : R
h : IsSumSq s
⊢ motive s h

Tactic:
match h with
  | .zero        => zero
  | .sq_add _ hs => sq_add (.mul_self _) hs (rec' zero sq_add _)

Premises used: IsSquare.mul_self, _private.0.IsSumSq.rec'.match_1
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
zero : IsSumSq (0 + s₂)
sq_add : ∀ (a : R) {s : R}, IsSumSq s → IsSumSq (s + s₂) → IsSumSq (a * a + s + s₂)
⊢ IsSumSq (s₁ + s₂)

Tactic:
induction h₁
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
⊢ IsSumSq (0 + s₂)

Tactic:
simp_all [add_assoc, sq_add]

Premises used: add_assoc, IsSumSq.sq_add
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
a s : R
hs : IsSumSq s
hs_ih : IsSumSq (s + s₂)
⊢ IsSumSq (a * a + s + s₂)

Tactic:
simp_all [add_assoc, sq_add]

Premises used: add_assoc, IsSumSq.sq_add
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : AddMonoid T
inst_1 : Mul T
s : T
⊢ Membership.mem (γ := AddSubmonoid T) (sumSq T) s ↔ IsSumSq s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddZeroClass R
inst_1 : Mul R
a : R
⊢ IsSumSq (a * a)

Tactic:
simpa using sq_add a zero

Premises used: IsSumSq.zero, IsSumSq.sq_add
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddZeroClass R
inst_1 : Mul R
x : R
hx : IsSquare x
⊢ IsSumSq x

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddZeroClass R
inst_1 : MulOneClass R
⊢ IsSumSq.{u_1} (R := R) 1

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
⊢ Eq (α := AddSubmonoid R) (closure {x : R | IsSquare x}) (sumSq R)

Tactic:
closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)

Premises used: IsSquare.isSumSq, AddSubmonoid.closure_eq_of_le
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
refine :
  ∀ (x : R) (hx : Membership.mem (γ := AddSubmonoid R) (sumSq R) x),
    Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) x
⊢ Eq (α := AddSubmonoid R) (closure {x : R | IsSquare x}) (sumSq R)

Tactic:
refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)

Premises used: AddSubmonoid.closure_eq_of_le
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (sumSq R) x
zero : Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) 0
sq_add :
  ∀ (a : R) {s : R},
    IsSumSq s →
      Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) s →
        Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) (a * a + s)
⊢ Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) x

Tactic:
induction hx
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
⊢ Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x a s : R
hs : IsSumSq s
hs_ih : Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) s
⊢ Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) (a * a + s)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
ι : Type u_2
I : Finset ι
s : ι → R
hs : ∀ i ∈ I, IsSumSq (s i)
⊢ IsSumSq.{u_1} (R := R) (∑ i ∈ I, s i)

Tactic:
simpa using sum_mem (S := AddSubmonoid.sumSq _) hs

Premises used: sum_mem
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSquare (x i)
⊢ IsSumSq.{u_1} (R := R) (∑ i ∈ I, x i)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
ι : Type u_2
I : Finset ι
a : ι → R
⊢ IsSumSq.{u_1} (R := R) (∑ i ∈ I, a i * a i)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
I : Finset ι
a : ι → R
⊢ IsSumSq.{u_1} (R := R) (∑ i ∈ I, HPow.hPow (β := ℕ) (a i) 2)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
⊢ Eq (α := AddSubmonoid T) (toAddSubmonoid (sumSq T)) (AddSubmonoid.sumSq T)

Tactic:
simp [sumSq, ← AddSubmonoid.closure_isSquare,
    Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid]

Premises used: NonUnitalSubsemiring.sumSq, AddSubmonoid.closure_isSquare, Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
s : T
⊢ Membership.mem (γ := NonUnitalSubsemiring T) (sumSq T) s ↔ IsSumSq s

Tactic:
simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]

Premises used: NonUnitalSubsemiring.mem_toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
h : ∀ (x : T), x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x
⊢ (↑(sumSq T) : Set T) = {s : T | IsSumSq s}

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
x : T
⊢ x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
⊢ Eq (α := NonUnitalSubsemiring T) (closure {x : T | IsSquare x}) (sumSq T)

Tactic:
simp [sumSq, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

Premises used: NonUnitalSubsemiring.sumSq, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : NonAssocSemiring R
n : ℕ
zero : IsSumSq.{u_2} (R := R) (↑0 : R)
succ : ∀ (n : ℕ), IsSumSq.{u_2} (R := R) (↑n : R) → IsSumSq.{u_2} (R := R) (↑(n + 1) : R)
⊢ IsSumSq.{u_2} (R := R) (↑n : R)

Tactic:
induction n
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ IsSumSq.{u_2} (R := R) (↑0 : R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_2
inst : NonAssocSemiring R
n : ℕ
h : IsSumSq.{u_2} (R := R) (↑n : R)
⊢ IsSumSq.{u_2} (R := R) (↑(n + 1) : R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
n : ℕ
⊢ IsSumSq n

Tactic:
IsSumSq.natCast n

Premises used: IsSumSq.natCast
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.sumSq R) s₁

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.sumSq R) s₂

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.SumsOfSquares
Goal:
R : Type u_1
inst : NonUnitalCommSemiring R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ * s₂)

Tactic:
simpa using mul_mem (by simpa : _ ∈ NonUnitalSubsemiring.sumSq R) (by simpa)

Premises used: MulMemClass.mul_mem