awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
zero : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 0
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 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 →
      ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x)
        (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 + y
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
zero : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 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 →
        ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x)
          (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 + y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
have neg : ∀ (x : R),
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
    ∀ (hL : ∃ (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
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
inst : NonAssocRing R
n : ℤ
s : Set R
⊢ Eq (α := Subring R) (closure (insert (↑n : R) s)) (closure s)
have rw : Eq (α := Subring R) (closure {(↑n : R)} ⊔ closure s) (closure s)
Tactic: rw [Set.insert_eq, closure_union]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subring 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.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := Subring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := Subring 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.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun (x1 x2 : Subring R) ↦ x1 ≤ x2) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), (S i).toAddSubgroup) ⋯ ⋯
⊢ Membership.mem (γ := Subring 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.Subring.Basic (hypothesis)
Goal:
R : Type u
inst : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subring 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.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
⊢ (↑f.range : 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_range, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing 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.range : 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_range, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
⊢ Membership.mem.{v, v} (α := S) (γ := Subring S) (closure ((⇑f : (a : R) → S) '' s)) ((f : (a : R) → S) x : S)
have rw : ∃ (x_1 : R),
  Membership.mem (γ := Subring R) (closure s) x_1 ∧
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)
Tactic: rw [← f.map_closure, Subring.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)
have rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)
have rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
s_1 t : Subring R_1
R : Type u
S : Type v
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_5 : SetLike σR R
inst_6 : SetLike σS S
inst_7 : SubsemiringClass σR R
inst_8 : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)
y : S
hy : y ∈ s
⊢ Membership.mem.{u, u_1} (α := R) s' (((↑e.symm : S →+* R) : (a : S) → R) y : R)
have obtain : ∀ (x : R) (hy : Membership.mem.{v, u_2} (α := S) s ((e : (a : R) → S) x : S)),
  Membership.mem.{u, u_1} (α := R) s' (((↑e.symm : S →+* R) : (a : S) → R) ((e : (a : R) → S) x : S) : R)
Tactic: obtain ⟨x, rfl⟩ := e.surjective y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x
have have : ∀ (h0 : C 0), C x
Tactic: have h0 : C 0 := add_neg_cancel (1 : R) ▸ ha h1 hneg1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
⊢ C x
have rcases : ∀ (L : List (List R)) (HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1)
  (hx : Membership.mem (γ := Subring R) (closure s) (List.map List.prod L).sum), C (List.map List.prod L).sum
Tactic: rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod L).sum
have cons : ∀ (hd : List R) (tl : List (List R)) (ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum)
  (HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod (hd :: tl)).sum
Tactic: induction L with
  | nil => exact h0
  | cons hd tl ih => ?_
Cleared hypotheses: L, HL
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum
have HL₁ : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
Tactic: rw [List.forall_mem_cons] at 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
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (List.map List.prod (hd :: tl)).sum
have rw : C (hd.prod + (List.map List.prod tl).sum)
Tactic: rw [List.map_cons, List.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum
have cons : C hd.prod
Tactic: suffices C (List.prod hd) by
    rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : ∀ (HL : ∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1), C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C hd.prod
have cons : ∀ (HL : ∀ y ∈ hd, y ∈ s ∨ y = -1), C hd.prod
Tactic: replace HL := HL.1
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
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ C hd.prod
have cons : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = L.prod), C hd.prod
Tactic: rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
cons : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = L.prod), C hd.prod
⊢ C hd.prod
have cons₁ : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = -L.prod), C hd.prod
Tactic: rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
cons : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = L.prod), C hd.prod
cons₁ : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = -L.prod), C hd.prod
⊢ C hd.prod
have rsuffices : ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)
Tactic: rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C hd.prod
have cons : C L.prod
Tactic: rw [HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (hd :: tl).prod
have HL'₁ : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
Tactic: rw [List.forall_mem_cons] at 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
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd :: tl).prod
have cons : C (hd * tl.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
⊢ C L.prod
have cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (List.prod [])
Tactic: induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)
Cleared hypotheses: L, HL'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (List.prod [])
⊢ C L.prod
have cons₁ : ∀ (hd : R) (tl : List R) (ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod) (HL' : ∀ x ∈ hd :: tl, x ∈ s), C (hd :: tl).prod
Tactic: induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)
Cleared hypotheses: L, HL'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod
have cons : C (-L.prod)
Tactic: rw [HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (-(hd :: tl).prod)
have cons : C (hd * -tl.prod)
Tactic: rw [List.prod_cons, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (hd * -tl.prod)
have HL'₁ : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
Tactic: rw [List.forall_mem_cons] at 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
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
⊢ C (-L.prod)
have cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (-List.prod [])
Tactic: induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)
Cleared hypotheses: L, HL'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (-List.prod [])
⊢ C (-L.prod)
have cons₁ : ∀ (hd : R) (tl : List R) (ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)) (HL' : ∀ x ∈ hd :: tl, x ∈ s),
  C (-(hd :: tl).prod)
Tactic: induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)
Cleared hypotheses: L, HL'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)
have cons : ∀ (hd : R) (tl : List R)
  (ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod))
  (HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1),
  ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: induction hd with
  | nil => exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
  | cons hd tl ih => ?_
Cleared hypotheses: hd, HL
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have HL₁ : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
Tactic: rw [List.forall_mem_cons] at 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
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : tl.prod = L.prod),
  ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases ih HL.2 with ⟨L, HL', HP | HP⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
cons :
  ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : tl.prod = L.prod),
    ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons₁ : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : tl.prod = -L.prod),
  ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases ih HL.2 with ⟨L, HL', HP | HP⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons : ∀ (hhd : hd ∈ s), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases HL.1 with hhd | hhd