awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := Subring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s), Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
have one : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1
Tactic: induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := Subring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s), Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0
one : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
have add : ∀ (x y : R),
  Membership.mem (γ := Subring R) (closure s) x →
    Membership.mem (γ := Subring R) (closure s) y →
      ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
        (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x + y)
Tactic: induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := Subring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s), Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0
one : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1
add :
  ∀ (x y : R),
    Membership.mem (γ := Subring R) (closure s) x →
      Membership.mem (γ := Subring R) (closure s) y →
        ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
          (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
          Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x + y)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
have neg : ∀ (x : R),
  Membership.mem (γ := Subring R) (closure s) x →
    ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x),
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x)
Tactic: induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := Subring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s), Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0
one : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1
add :
  ∀ (x y : R),
    Membership.mem (γ := Subring R) (closure s) x →
      Membership.mem (γ := Subring R) (closure s) y →
        ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
          (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
          Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x + y)
neg :
  ∀ (x : R),
    Membership.mem (γ := Subring R) (closure s) x →
      ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x),
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
have mul : ∀ (x y : R) (_hx : Membership.mem (γ := Subring R) (closure s) x) (_hy : Membership.mem (γ := Subring R) (closure s) y)
  (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
  (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x * y)
Tactic: induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
⊢ Membership.mem (γ := Subring R) (closure s) x
have mem : ∀ (x : R) (h : x ∈ s), Membership.mem (γ := Subring R) (closure s) x
Tactic: induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
mem : ∀ (x : R) (h : x ∈ s), Membership.mem (γ := Subring R) (closure s) x
⊢ Membership.mem (γ := Subring R) (closure s) x
have mem₁ : Membership.mem (γ := Subring R) (closure s) 1
Tactic: induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
mem : ∀ (x : R) (h : x ∈ s), Membership.mem (γ := Subring R) (closure s) x
mem₁ : Membership.mem (γ := Subring R) (closure s) 1
⊢ Membership.mem (γ := Subring R) (closure s) x
have mem₂ : ∀ (x y : R),
  Membership.mem (γ := Submonoid R) (Submonoid.closure s) x →
    Membership.mem (γ := Submonoid R) (Submonoid.closure s) y →
      ∀ (h₁ : Membership.mem (γ := Subring R) (closure s) x) (h₂ : Membership.mem (γ := Subring R) (closure s) y),
        Membership.mem (γ := Subring R) (closure s) (x * y)
Tactic: induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
⊢ Membership.mem (γ := Subring R) (closure s) x
have mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)), Membership.mem (γ := Subring R) (closure s) x
Tactic: induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | zero => exact zero_mem _
      | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | neg _ _ h => exact neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)), Membership.mem (γ := Subring R) (closure s) x
⊢ Membership.mem (γ := Subring R) (closure s) x
have zero : Membership.mem (γ := Subring R) (closure s) 0
Tactic: induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | zero => exact zero_mem _
      | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | neg _ _ h => exact neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)), Membership.mem (γ := Subring R) (closure s) x
zero : Membership.mem (γ := Subring R) (closure s) 0
⊢ Membership.mem (γ := Subring R) (closure s) x
have add : ∀ (x y : R),
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y →
      ∀ (h₁ : Membership.mem (γ := Subring R) (closure s) x) (h₂ : Membership.mem (γ := Subring R) (closure s) y),
        Membership.mem (γ := Subring R) (closure s) (x + y)
Tactic: induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | zero => exact zero_mem _
      | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | neg _ _ h => exact neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)), Membership.mem (γ := Subring R) (closure s) x
zero : Membership.mem (γ := Subring R) (closure s) 0
add :
  ∀ (x y : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y →
        ∀ (h₁ : Membership.mem (γ := Subring R) (closure s) x) (h₂ : Membership.mem (γ := Subring R) (closure s) y),
          Membership.mem (γ := Subring R) (closure s) (x + y)
⊢ Membership.mem (γ := Subring R) (closure s) x
have neg : ∀ (x : R),
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
    ∀ (h : Membership.mem (γ := Subring R) (closure s) x), Membership.mem (γ := Subring R) (closure s) (-x)
Tactic: induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | zero => exact zero_mem _
      | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | neg _ _ h => exact neg_mem h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
have hx₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
Tactic: rw [mem_closure_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : x_1 ∈ (↑(Submonoid.closure s) : Set R)
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
have mem : ∀ (l : List R) (hl : ∀ y ∈ l, y ∈ s) (h : l.prod = x_1),
  ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
Tactic: obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1 + y
have add : ∀ (L : List (List R)) (HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) (HL2 : (List.map List.prod L).sum = x_1)
  (M : List (List R)) (HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1) (HM2 : (List.map List.prod M).sum = y),
  ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1 + y
Tactic: obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x_1
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y
⊢ (List.map List.prod (L ++ M)).sum = x_1 + y
have rw : (List.map List.prod L ++ List.map List.prod M).sum = x_1 + y
Tactic: rw [List.map_append, List.sum_append, HL2, HM2]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x_1
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y
rw : (List.map List.prod L ++ List.map List.prod M).sum = x_1 + y
⊢ (List.map List.prod (L ++ M)).sum = x_1 + y
have rw₁ : (List.map List.prod L).sum + (List.map List.prod M).sum = x_1 + y
Tactic: rw [List.map_append, List.sum_append, HL2, HM2]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x_1
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y
rw : (List.map List.prod L ++ List.map List.prod M).sum = x_1 + y
rw₁ : (List.map List.prod L).sum + (List.map List.prod M).sum = x_1 + y
⊢ (List.map List.prod (L ++ M)).sum = x_1 + y
have rw₂ : x_1 + (List.map List.prod M).sum = x_1 + y
Tactic: rw [List.map_append, List.sum_append, HL2, HM2]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x_1
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y
rw : (List.map List.prod L ++ List.map List.prod M).sum = x_1 + y
rw₁ : (List.map List.prod L).sum + (List.map List.prod M).sum = x_1 + y
rw₂ : x_1 + (List.map List.prod M).sum = x_1 + y
⊢ (List.map List.prod (L ++ M)).sum = x_1 + y
have rw₃ : x_1 + y = x_1 + y
Tactic: rw [List.map_append, List.sum_append, HL2, HM2]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x_1
have neg : ∀ (L : List (List R)) (hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1),
  ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x_1
Tactic: obtain ⟨L, hL⟩ := hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
have mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
  ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
Tactic: induction hx using AddSubgroup.closure_induction with
  | mem _ hx =>
    obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
    exact ⟨[l], by simp_all⟩
  | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
  | add _ _ _ _ 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]⟩
  | neg _ _ hL =>
    obtain ⟨L, hL⟩ := hL
    exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem :
  ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
have zero : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 0
Tactic: induction hx using AddSubgroup.closure_induction with
  | mem _ hx =>
    obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
    exact ⟨[l], by simp_all⟩
  | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
  | add _ _ _ _ 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]⟩
  | neg _ _ hL =>
    obtain ⟨L, hL⟩ := hL
    exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩
Cleared hypotheses: hx