awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
mp :
  ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
have mp₁ : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0
Tactic: induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | add x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
mp :
  ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
mp₁ : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
have mp₂ : ∀ (x y : R),
  Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x →
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) y →
      ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x)
        (hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y),
        ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y
Tactic: induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | add x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
n : ℕ
s : Set R
⊢ Eq (α := Subsemiring R) (closure (insert (↑n : R) s)) (closure s)
have rw : Eq (α := Subsemiring R) (closure {(↑n : R)} ⊔ closure s) (closure s)
Tactic: rw [Set.insert_eq, closure_union]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subsemiring R
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)
have a : (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) ⋯ (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
have suffices : ⨆ (i : ι), S i ≤ U
Tactic: suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (hypothesis)
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
have this : Nonempty.{u + 1} (↑S : Type u)
Tactic: haveI : Nonempty S := Sne.to_subtype
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ (↑f.rangeS : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
have rw : Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
Tactic: rw [coe_rangeS, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
rw :
  Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
⊢ (↑f.rangeS : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
have rw₁ : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ ↔
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
Tactic: rw [coe_rangeS, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.rangeS
⊢ (↑((fun (x : R) ↦ ((f.rangeSRestrict : (a : R) → ↥f.rangeS) x : ↥f.rangeS))
          ((fun (x : ↥f.rangeS) ↦ (g ∘ (⇑f.rangeS.subtype : (a : ↥f.rangeS) → S)) x) x)) :
      S) =
    (↑x : S)
have let : ∀ (x' : R) (hx' : (f : (a : R) → S) x' = (↑x : S)),
  (↑((fun (x : R) ↦ ((f.rangeSRestrict : (a : R) → ↥f.rangeS) x : ↥f.rangeS))
          ((fun (x : ↥f.rangeS) ↦ (g ∘ (⇑f.rangeS.subtype : (a : ↥f.rangeS) → S)) x) x)) :
      S) =
    (↑x : S)
Tactic: let ⟨x', hx'⟩ := RingHom.mem_rangeS.mp x.prop
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
s : S
inst_2 : AddSubmonoidWithOneClass S R
n : ℕ
⊢ (↑n : R) ∈ s
have zero : (↑0 : R) ∈ s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
s : S
inst_2 : AddSubmonoidWithOneClass S R
n : ℕ
zero : (↑0 : R) ∈ s
⊢ (↑n : R) ∈ s
have succ : ∀ (n : ℕ), (↑n : R) ∈ s → (↑(n + 1) : R) ∈ s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
inst_2 : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst_3 : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ s
have rw : (↑(OfNat.ofNat n) : R) ∈ s
Tactic: rw [← Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
p q : Subsemiring R
h : Eq.{u + 1} (α := Set R) ((fun (s : Subsemiring R) ↦ s.carrier) p) ((fun (s : Subsemiring R) ↦ s.carrier) q)
⊢ p = q
have mk : ∀ (toSubmonoid : Submonoid R)
  (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem' : 0 ∈ toSubmonoid.carrier)
  (h :
    Eq.{u + 1} (α := Set R)
      ((fun (s : Subsemiring R) ↦ s.carrier)
        { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
      ((fun (s : Subsemiring R) ↦ s.carrier) q)),
  { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
q : Subsemiring R
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier) q)
⊢ { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } = q
have mk : ∀ (toSubmonoid_1 : Submonoid R)
  (add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier)
  (zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier)
  (h :
    Eq.{u + 1} (α := Set R)
      ((fun (s : Subsemiring R) ↦ s.carrier)
        { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
      ((fun (s : Subsemiring R) ↦ s.carrier)
        { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })),
  { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } =
    { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
toSubmonoid_1 : Submonoid R
add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier
zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })
⊢ { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } =
    { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 }
have mk : toSubmonoid = toSubmonoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.MulOpposite (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set R
⊢ Eq (α := Subsemiring Rᵐᵒᵖ) (Subsemiring.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))
have 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ᵐᵒᵖ)})
Tactic: simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.MulOpposite (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : 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ᵐᵒᵖ)})
have e_a : ∀ (a : Subsemiring Rᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Rᵐᵒᵖ)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.MulOpposite (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ Eq (α := Subsemiring R) (Subsemiring.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))
have rw : Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
Tactic: rw [← op_inj, op_unop, op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.MulOpposite (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw : Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subsemiring.MulOpposite (goal)
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))
⊢ Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw₁ : Eq (α := Subsemiring Rᵐᵒᵖ) (closure s) (closure ((fun (x : Rᵐᵒᵖ) ↦ x) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
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
⊢ IsSumSq (x + s)
have rcases : ∀ (w : R), IsSumSq (w * w + s)
Tactic: rcases hx with ⟨_, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ + s₂)
have zero : IsSumSq (0 + s₂)
Tactic: induction h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
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₂)
⊢ IsSumSq (s₁ + s₂)
have sq_add : ∀ (a : R) {s : R}, IsSumSq s → IsSumSq (s + s₂) → IsSumSq (a * a + s + s₂)
Tactic: induction h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
⊢ Eq (α := AddSubmonoid R) (closure {x : R | IsSquare x}) (sumSq R)
have refine : ∀ (x : R) (hx : Membership.mem (γ := AddSubmonoid R) (sumSq R) x),
  Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) x
Tactic: refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (sumSq R) x
⊢ Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) x
have zero : Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) 0
Tactic: induction hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
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
⊢ Membership.mem (γ := AddSubmonoid R) (closure {x : R | IsSquare x}) x
have 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)
Tactic: induction hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
T : Type u_2
inst : NonUnitalCommSemiring T
⊢ (↑(sumSq T) : Set T) = {s : T | IsSumSq s}
have h : ∀ (x : T), x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
n : ℕ
⊢ IsSumSq.{u_2} (R := R) (↑n : R)
have zero : IsSumSq.{u_2} (R := R) (↑0 : R)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
n : ℕ
zero : IsSumSq.{u_2} (R := R) (↑0 : R)
⊢ IsSumSq.{u_2} (R := R) (↑n : R)
have succ : ∀ (n : ℕ), IsSumSq.{u_2} (R := R) (↑n : R) → IsSumSq.{u_2} (R := R) (↑(n + 1) : R)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
T : Type u_2
inst : CommSemiring T
⊢ (↑(sumSq T) : Set T) = {s : T | IsSumSq s}
have h : ∀ (x : T), x ∈ (↑(sumSq T) : Set T) ↔ Membership.mem (γ := Set T) {s : T | IsSumSq s} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
T : Type u_2
inst : CommSemiring T
⊢ Eq (α := Subsemiring T) (closure {x : T | IsSquare x}) (sumSq T)
have apply_fun : Eq (α := NonUnitalSubsemiring T) (toNonUnitalSubsemiring (closure {x : T | IsSquare x}))
  (toNonUnitalSubsemiring (sumSq T))
Tactic: apply_fun toNonUnitalSubsemiring using toNonUnitalSubsemiring_injective
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : R
hs : IsSumSq s
⊢ 0 ≤ s
have zero : LE.le.{u_2} (α := R) 0 0
Tactic: induction hs using IsSumSq.rec' with
  | zero          => simp
  | sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Ring.SumsOfSquares (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : R
hs : IsSumSq s
zero : LE.le.{u_2} (α := R) 0 0
⊢ 0 ≤ s
have sq_add : ∀ {x s : R} (hx : IsSquare x), IsSumSq s → ∀ (h : 0 ≤ s), 0 ≤ x + s
Tactic: induction hs using IsSumSq.rec' with
  | zero          => simp
  | sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : Eq.{u_1 + 1} (α := R) ((fun (a : R) ↦ n • a) a) ((fun (a : R) ↦ n • a) b)
⊢ a = b
have w₁ : a = b ∨ n = 0
Tactic: simp only [nsmul_eq_mul, mul_eq_mul_left_iff, Nat.cast_eq_zero] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
⊢ HPow.hPow (α := M) ((f : (a : R) → M) (-1) : M) (Nat.succ 1) = 1
have rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (HPow.hPow (α := R) (-1) (Nat.succ 1)) : M) (1 : M)
Tactic: rw [← map_pow, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (HPow.hPow (α := R) (-1) (Nat.succ 1)) : M) (1 : M)
⊢ HPow.hPow (α := M) ((f : (a : R) → M) (-1) : M) (Nat.succ 1) = 1
have rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) 1 : M) (1 : M)
Tactic: rw [← map_pow, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (HPow.hPow (α := R) (-1) (Nat.succ 1)) : M) (1 : M)
rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) 1 : M) (1 : M)
⊢ HPow.hPow (α := M) ((f : (a : R) → M) (-1) : M) (Nat.succ 1) = 1
have rw₂ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [← map_pow, neg_one_sq, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x : R
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-x) : M) ((f : (a : R) → M) x : M)
have rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-1 * x) : M) ((f : (a : R) → M) x : M)
Tactic: rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-1 * x) : M) ((f : (a : R) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-x) : M) ((f : (a : R) → M) x : M)
have rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : R) → M) (-1) : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
Tactic: rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-1 * x) : M) ((f : (a : R) → M) x : M)
rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : R) → M) (-1) : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-x) : M) ((f : (a : R) → M) x : M)
have rw₂ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
Tactic: rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-1 * x) : M) ((f : (a : R) → M) x : M)
rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : R) → M) (-1) : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
rw₂ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : R) → M) x : M) = (f : (a : R) → M) x
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-x) : M) ((f : (a : R) → M) x : M)
have rw₃ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) x : M) ((f : (a : R) → M) x : M)
Tactic: rw [← neg_one_mul, map_mul, map_neg_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x y : R
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (x - y) : M) ((f : (a : R) → M) (y - x) : M)
have rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-(x - y)) : M) ((f : (a : R) → M) (y - x) : M)
Tactic: rw [← map_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Torsion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : Monoid M
inst_2 : IsMulTorsionFree M
f : R →* M
x y : R
rw : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (-(x - y)) : M) ((f : (a : R) → M) (y - x) : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (x - y) : M) ((f : (a : R) → M) (y - x) : M)
have rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : R) → M) (y - x) : M) ((f : (a : R) → M) (y - x) : M)
Tactic: rw [← map_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalNonAssocSemiring α
have zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.nonUnitalNonAssocSemiring _
-- Lean 4 proof step from Mathlib.Algebra.Ring.TransferInstance (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
zero₁ : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ NonUnitalNonAssocSemiring α
have add₁ : ∀ (x y : α), (e : (a : α) → β) (x + y) = HAdd.hAdd (α := β) (β := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.nonUnitalNonAssocSemiring _