[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
p q : NonUnitalSubring 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✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
q : NonUnitalSubring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } =
    (fun s => s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toNonUnitalSubsemiring
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
[PROOFSTEP]
exact SetLike.coe_injective h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
s : NonUnitalSubring R
x : { x // x ∈ s }
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f✝ f : R →ₙ+* S
⊢ range f = NonUnitalSubring.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f✝ f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ NonUnitalSubring.map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g (range f) = range (comp g f)
[PROOFSTEP]
simpa only [range_eq_map] using (⊤ : NonUnitalSubring R).map_map g f
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
x : R
⊢ x ∈ ↑⊥ ↔ x = 0
[PROOFSTEP]
rw [coe_bot, Set.mem_singleton_iff]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ (t : NonUnitalSubring R) (_ : t ∈ s), toSubsemigroup t) = ⋂ (t : NonUnitalSubring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ (t : NonUnitalSubring R) (_ : t ∈ s), toAddSubgroup t) = ⋂ (t : NonUnitalSubring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
S : ι → NonUnitalSubring R
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
S : ι → NonUnitalSubring R
x : R
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ p { val := b, property := hb }
[PROOFSTEP]
refine' Exists.elim _ fun (hb : b ∈ closure s) (hc : p ⟨b, hb⟩) => hc
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∃ x, p { val := b, property := x }
[PROOFSTEP]
refine' closure_induction hb (fun x hx => ⟨subset_closure hx, Hs x hx⟩) ⟨zero_mem (closure s), H0⟩ _ _ _
[GOAL]
case refine'_1
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x y : R),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x + y, property := x_1 }
[PROOFSTEP]
rintro x y ⟨hx, hpx⟩ ⟨hy, hpy⟩
[GOAL]
case refine'_1.intro.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x y : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
hy : y ∈ closure s
hpy : p { val := y, property := hy }
⊢ ∃ x_1, p { val := x + y, property := x_1 }
[PROOFSTEP]
exact ⟨add_mem hx hy, Hadd _ _ hpx hpy⟩
[GOAL]
case refine'_2
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x : R), (∃ x_1, p { val := x, property := x_1 }) → ∃ x_1, p { val := -x, property := x_1 }
[PROOFSTEP]
rintro x ⟨hx, hpx⟩
[GOAL]
case refine'_2.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
⊢ ∃ x_1, p { val := -x, property := x_1 }
[PROOFSTEP]
exact ⟨neg_mem hx, Hneg _ hpx⟩
[GOAL]
case refine'_3
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
⊢ ∀ (x y : R),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x * y, property := x_1 }
[PROOFSTEP]
rintro x y ⟨hx, hpx⟩ ⟨hy, hpy⟩
[GOAL]
case refine'_3.intro.intro
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
p : { x // x ∈ closure s } → Prop
a : { x // x ∈ closure s }
Hs : ∀ (x : R) (hx : x ∈ s), p { val := x, property := (_ : x ∈ ↑(closure s)) }
H0 : p 0
Hadd : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x + y)
Hneg : ∀ (x : { x // x ∈ closure s }), p x → p (-x)
Hmul : ∀ (x y : { x // x ∈ closure s }), p x → p y → p (x * y)
b : R
hb : b ∈ closure s
x y : R
hx : x ∈ closure s
hpx : p { val := x, property := hx }
hy : y ∈ closure s
hpy : p { val := y, property := hy }
⊢ ∃ x_1, p { val := x * y, property := x_1 }
[PROOFSTEP]
exact ⟨mul_mem hx hy, Hmul _ _ hpx hpy⟩
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
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
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 _) (Hadd_right a) (Hneg_right a) (Hmul_right a)
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
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
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) _ _ _
[GOAL]
case refine'_1
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
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
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
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
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
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
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
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
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]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
⊢ 0 * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [zero_mul q]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ (p₁ + p₂) * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [add_mul p₁ p₂ q]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
p₁ p₂ : R
ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihp₁ ihp₂
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
have f : -x * q = -(x * q) := by simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x * q = -(x * q)
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : -x * q = -(x * q)
⊢ -x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x✝ y : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q : R
hq : q ∈ ↑(Subsemigroup.closure s)
x : R
hx : x * q ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : -x * q = -(x * q)
⊢ -(x * q) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hx
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [mul_zero x]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.zero_mem _
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * (q₁ + q₂) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [mul_add x q₁ q₂]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
q₁ q₂ : R
ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.add_mem _ ihq₁ ihq₂
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * -z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
have f : x * -z = -(x * z) := by simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x * -z = -(x * z)
[PROOFSTEP]
simp
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : x * -z = -(x * z)
⊢ x * -z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
rw [f]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : Set R
x✝ : R
h : x✝ ∈ closure s
x y : R
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
z : R
hz : x * z ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
f : x * -z = -(x * z)
⊢ -(x * z) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
[PROOFSTEP]
apply AddSubgroup.neg_mem _ hz
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y : { x // x ∈ closure s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x y : { x // x ∈ closure s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [NonUnitalSubring.val_mul]
[GOAL]
case a
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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 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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ 0 * x = x * 0
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (closure s)
x✝ y : { x // x ∈ closure s }
x : R
⊢ x * 0 = 0 * x
[PROOFSTEP]
simp only [mul_zero, zero_mul]
[GOAL]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R✝ : Type u
S : Type v
T : Type u_1
inst✝⁴ : NonUnitalNonAssocRing R✝
inst✝³ : NonUnitalNonAssocRing S
inst✝² : NonUnitalNonAssocRing T
inst✝¹ : NonUnitalRingHomClass F R✝ S
g : S →ₙ+* T
f : R✝ →ₙ+* S
R : Type u
inst✝ : NonUnitalRing R
s : Set R
hcomm : ∀ (a : R), a ∈ s → ∀ (b : R), b ∈ s → a * b = b * a
src✝ : NonUnitalRing { x // x ∈ closure s } := toNonUnitalRing (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]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : NonUnitalSubring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f : R →ₙ+* S
s : NonUnitalSubring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring 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]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
    (Subsemigroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (AddSubgroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices (⨆ i, S i) ≤ U by simpa using @this x
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa using @this x
[GOAL]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i)) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i)))
    (_ : ↑(⨆ (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]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubring 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]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring 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]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring 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]
F : Type w
R : Type u
S✝ : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S✝
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S✝
g : S✝ →ₙ+* T
f : R →ₙ+* S✝
S : Set (NonUnitalSubring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : NonUnitalSubring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
inst✝¹ : NonUnitalNonAssocRing T
inst✝ : NonUnitalRingHomClass F R S
g : S →ₙ+* T
f✝ : R →ₙ+* S
s : NonUnitalSubring R
f : R →ₙ+* S
⊢ ↑(range f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_range, coe_top]
[GOAL]
F : Type w
R : Type u
S : Type v
T : Type u_1
inst✝³ : NonUnitalRing R
inst✝² : NonUnitalRing S
inst✝¹ : NonUnitalRing T
inst✝ : NonUnitalRingHomClass F R S
g✝ : S →ₙ+* T
f✝ : R →ₙ+* S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g ↑f
src✝ : R →ₙ+* { x // x ∈ NonUnitalRingHom.range f } := NonUnitalRingHom.rangeRestrict f
x : { x // x ∈ NonUnitalRingHom.range f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']
