[GOAL]
R : Type u
S : Type v
T : Type w
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ ↑n ∈ s
[PROOFSTEP]
simp only [← zsmul_one, zsmul_mem, one_mem]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
p q : Subring R
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
q : Subring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h : (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ } = (fun s => s.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
toSubsemiring✝¹ : Subsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toSubsemiring✝¹.carrier → -x ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSubsemiring
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
toSubsemiring✝¹ : Subsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toSubsemiring✝¹.carrier → -x ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toSubsemiring := toSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
[PROOFSTEP]
exact SetLike.ext' h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -x✝ ∈ s.carrier
[PROOFSTEP]
rw [← neg_one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier
[PROOFSTEP]
exact mul_mem hneg h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s✝ : Subring R
f : R →+* S
s : Subring R
y : S
⊢ (∃ x x_1, ↑f x = y) ↔ ∃ x, x ∈ s ∧ ↑f x = y
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
⊢ range f = Subring.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ Subring.map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f : R →+* S
⊢ Subring.map g (range f) = range (comp g f)
[PROOFSTEP]
simpa only [range_eq_map] using (⊤ : Subring R).map_map g f
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set (Subring R)
⊢ ↑(⨅ (t : Subring R) (_ : t ∈ s), t.toSubmonoid) = ⋂ (t : Subring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set (Subring R)
⊢ ↑(⨅ (t : Subring R) (_ : t ∈ s), toAddSubgroup t) = ⋂ (t : Subring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
x : R
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ p a ha
[PROOFSTEP]
refine Exists.elim ?_ fun (ha : a ∈ closure s) (hc : p a ha) => hc
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∃ x, p a x
[PROOFSTEP]
refine
  closure_induction ha (fun m hm => ⟨subset_closure hm, Hs m hm⟩) ⟨zero_mem _, H0⟩ ⟨one_mem _, H1⟩ ?_
    (fun x hx => hx.elim fun hx' hx => ⟨neg_mem hx', Hneg _ _ hx⟩) ?_
[GOAL]
case refine_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x + y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨add_mem hx' hy', Hadd _ _ _ _ hx hy⟩)
[GOAL]
case refine_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : (x : R) → x ∈ closure s → Prop
Hs : ∀ (x : R) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
H0 : p 0 (_ : 0 ∈ closure s)
H1 : p 1 (_ : 1 ∈ closure s)
Hadd : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) (_ : x + y ∈ closure s)
Hneg : ∀ (x : R) (hx : x ∈ closure s), p x hx → p (-x) (_ : -x ∈ closure s)
Hmul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
a : R
ha : a ∈ closure s
⊢ ∀ (x y : R), (∃ x_1, p x x_1) → (∃ x, p y x) → ∃ x_1, p (x * y) x_1
[PROOFSTEP]
exact (fun x y hx hy => hx.elim fun hx' hx => hy.elim fun hy' hy => ⟨mul_mem hx' hy', Hmul _ _ _ _ hx hy⟩)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ p a b
[PROOFSTEP]
refine' closure_induction hb _ (H0_right _) (H1_right _) (Hadd_right a) (Hneg_right a) (Hmul_right a)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), x ∈ s → p a x
[PROOFSTEP]
refine' closure_induction ha Hs (fun x _ => H0_left x) (fun x _ => H1_left x) _ _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x + y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hadd_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
case refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → ∀ (x_1 : R), x_1 ∈ s → p (-x) x_1
[PROOFSTEP]
exact fun x hx z zs => Hneg_left x z (hx z zs)
[GOAL]
case refine'_3
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x * y) x_1
[PROOFSTEP]
exact fun x y H₁ H₂ z zs => Hmul_left x y z (H₁ z zs) (H₂ z zs)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
⊢ 0 * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [zero_mul q]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ (p₁ + p₂) * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [add_mul p₁ p₂ q]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihp₁ ihp₂
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
have f : -x * q = -(x * q) := by simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x * q = -(x * q)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : -x * q = -(x * q)
⊢ -x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q : R
hq : q ∈ ↑(Submonoid.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : -x * q = -(x * q)
⊢ -(x * q) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hx
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [mul_zero x]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * (q₁ + q₂) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [mul_add x q₁ q₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihq₁ ihq₂
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * -z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
have f : x * -z = -(x * z) := by simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x * -z = -(x * z)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : x * -z = -(x * z)
⊢ x * -z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)
f : x * -z = -(x * z)
⊢ -(x * z) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hz
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [Subring.coe_mul]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
refine'
  closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [mul_zero, zero_mul])
    (fun x => by simp only [mul_zero, zero_mul]) (fun x => by simp only [mul_one, one_mul])
    (fun x => by simp only [mul_one, one_mul]) (fun x y hxy => by simp only [mul_neg, neg_mul, hxy])
    (fun x y hxy => by simp only [mul_neg, neg_mul, hxy]) (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y h₁ h₂ => by rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]) fun x₁ x₂ y h₁ h₂ => by
    rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 0 * x = x * 0
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 0 = 0 * x
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 1 * x = x * 1
[PROOFSTEP]
simp only [mul_one, one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 1 = 1 * x
[PROOFSTEP]
simp only [mul_one, one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ -x * y = y * -x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x✝ y✝ : { x // x ∈ closure s }
x y : R
hxy : x * y = y * x
⊢ x * -y = -y * x
[PROOFSTEP]
simp only [mul_neg, neg_mul, hxy]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ + y) = (x₂ + y) * x₁
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ x₁ * x₂ * y = y * (x₁ * x₂)
[PROOFSTEP]
rw [← mul_assoc, ← h₁, mul_assoc x₁ y x₂, ← h₂, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : Ring { x // x ∈ closure s } := toRing (closure s)
x y✝ : { x // x ∈ closure s }
x₁ x₂ y : R
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y = y * x₁
⊢ x₁ * (x₂ * y) = x₂ * y * x₁
[PROOFSTEP]
rw [← mul_assoc, h₁, mul_assoc, h₂, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ (∀ (t : List R), t ∈ [l] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod [l]) = x
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
[PROOFSTEP]
clear_aux_decl
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
[PROOFSTEP]
tauto
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x : R
h : x ∈ closure s
⊢ (∀ (t : List R), t ∈ [] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod []) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝² : R
h : x✝² ∈ closure s
x y : R
x✝¹ :
  (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) y
l : List (List R)
hl1 : ∀ (t : List R), t ∈ l → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hl2 : List.sum (List.map List.prod l) = x
m : List (List R)
hm1 : ∀ (t : List R), t ∈ m → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hm2 : List.sum (List.map List.prod m) = y
⊢ List.sum (List.map List.prod (l ++ m)) = x + y
[PROOFSTEP]
simp [hl2, hm2]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ List.sum (List.map List.prod (List.map (List.cons (-1)) [])) = -List.sum (List.map List.prod [])
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ ∀ (head : List R) (tail : List (List R)),
    List.sum (List.map List.prod (List.map (List.cons (-1)) tail)) = -List.sum (List.map List.prod tail) →
      List.sum (List.map List.prod (List.map (List.cons (-1)) (head :: tail))) =
        -List.sum (List.map List.prod (head :: tail))
[PROOFSTEP]
simp (config := { contextual := true }) [List.map_cons, add_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (RingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (RingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : Subring R :=
  Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
    (Submonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (AddSubgroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices ⨆ i, S i ≤ U by intro h; simpa using (this h)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
h : x ∈ ⨆ (i : ι), S i
⊢ ∃ i, x ∈ S i
[PROOFSTEP]
simpa using (this h)
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
S : Set (Subring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Subring R
f : R →+* S
⊢ ↑(range f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_range, coe_top]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s t : Subring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ↑f
src✝ : R →+* { x // x ∈ RingHom.range f } := RingHom.rangeRestrict f
x : { x // x ∈ RingHom.range f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
have h0 : C 0 := add_neg_self (1 : R) ▸ ha h1 hneg1
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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
[PROOFSTEP]
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hx : List.sum (List.map List.prod L) ∈ closure s
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
clear hx
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
HL : ∀ (t : List R), t ∈ [] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod []))
[PROOFSTEP]
exact h0
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (t : List R), t ∈ hd :: tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
suffices C (List.prod hd) by
  rw [List.map_cons, List.sum_cons]
  exact ha this (ih HL.2)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
this : C (List.prod hd)
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
this : C (List.prod hd)
⊢ C (List.prod hd + List.sum (List.map List.prod tl))
[PROOFSTEP]
exact ha this (ih HL.2)
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (y : R), y ∈ x → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
replace HL := HL.1
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
tl : List (List R)
ih : (∀ (t : List R), t ∈ tl → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
clear ih tl
[GOAL]
case intro.intro.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ C (List.prod hd)
[PROOFSTEP]
obtain ⟨L, HL', HP | HP⟩ : ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod L)
[PROOFSTEP]
clear HP HL hd
[GOAL]
case intro.intro.cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.cons.intro.intro.inl.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (List.prod [])
[PROOFSTEP]
exact h1
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL' 
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case intro.intro.cons.intro.intro.inl.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (-List.prod L)
[PROOFSTEP]
clear HP HL hd
[GOAL]
case intro.intro.cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (-List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.cons.intro.intro.inr.nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (-List.prod [])
[PROOFSTEP]
exact hneg1
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (-List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL' 
[GOAL]
case intro.intro.cons.intro.intro.inr.cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[PROOFSTEP]
induction' hd with hd tl ih
[GOAL]
case nil
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd : List R
HL✝ : ∀ (y : R), y ∈ hd → y ∈ s ∨ y = -1
HL : ∀ (y : R), y ∈ [] → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod [] = List.prod L ∨ List.prod [] = -List.prod L)
[PROOFSTEP]
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
[GOAL]
case cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : ∀ (y : R), y ∈ hd :: tl → y ∈ s ∨ y = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case cons
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rcases ih HL.2 with ⟨L, HL', HP | HP⟩
[GOAL]
case cons.intro.intro.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case cons.intro.intro.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case cons.intro.intro.inl.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP]
[GOAL]
case cons.intro.intro.inl.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = -List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, neg_one_mul, HP]
[GOAL]
case cons.intro.intro.inr.inl
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact
  ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = -List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
[GOAL]
case cons.intro.intro.inr.inr
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), 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 : List R), t ∈ L✝ → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hd✝ : List R
HL✝ : ∀ (y : R), y ∈ hd✝ → y ∈ s ∨ y = -1
hd : R
tl : List R
ih :
  (∀ (y : R), y ∈ tl → y ∈ s ∨ y = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g ∈ G
[PROOFSTEP]
convert AddSubgroup.zsmul_mem G h k using 1
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = k • g
[PROOFSTEP]
simp
