case refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
r : R
hr : r ∈ I
y : S
x✝ : y ∈ ⊤
⊢ r • y ∈ Submodule.restrictScalars R (map (algebraMap R S) I)

case refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (x : S), x ∈ ↑(algebraMap R S) '' ↑I → x ∈ I • ⊤

case refine'_3
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ 0 ∈ I • ⊤

case refine'_4
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (x y : S), x ∈ I • ⊤ → y ∈ I • ⊤ → x + y ∈ I • ⊤

case refine'_5
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (a x : S), x ∈ I • ⊤ → a • x ∈ I • ⊤
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
⊢ I • ⊤ = Submodule.restrictScalars R (map (algebraMap R S) I)
refine'
  le_antisymm (Submodule.smul_le.mpr fun r hr y _ => _) fun x hx =>
    Submodule.span_induction hx _ _ _ _
case refine'_5
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ a • x ∈ I • ⊤
case refine'_5
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (a x : S), x ∈ I • ⊤ → a • x ∈ I • ⊤
intro a x hx
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ ∀ (r : R), r ∈ I → ∀ (n : S), n ∈ ⊤ → a • r • n ∈ I • ⊤

case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ ∀ (x y : S), a • x ∈ I • ⊤ → a • y ∈ I • ⊤ → a • (x + y) ∈ I • ⊤
case refine'_5
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ a • x ∈ I • ⊤
refine' Submodule.smul_induction_on hx _ _
case refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
r : R
hr : r ∈ I
y : S
x✝ : y ∈ ⊤
⊢ ↑(algebraMap R S) r * y ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
case refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
r : R
hr : r ∈ I
y : S
x✝ : y ∈ ⊤
⊢ r • y ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
rw [Algebra.smul_def]
no goals
case refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
r : R
hr : r ∈ I
y : S
x✝ : y ∈ ⊤
⊢ ↑(algebraMap R S) r * y ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
exact mul_mem_right _ _ (mem_map_of_mem _ hr)
case refine'_2.intro.intro
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x : R
hx : x ∈ ↑I
⊢ ↑(algebraMap R S) x ∈ I • ⊤
case refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (x : S), x ∈ ↑(algebraMap R S) '' ↑I → x ∈ I • ⊤
rintro _ ⟨x, hx, rfl⟩
case refine'_2.intro.intro
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x : R
hx : x ∈ ↑I
⊢ x • 1 ∈ I • ⊤
case refine'_2.intro.intro
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x : R
hx : x ∈ ↑I
⊢ ↑(algebraMap R S) x ∈ I • ⊤
rw [← mul_one (algebraMap R S x), ← Algebra.smul_def]
no goals
case refine'_2.intro.intro
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x : R
hx : x ∈ ↑I
⊢ x • 1 ∈ I • ⊤
exact Submodule.smul_mem_smul hx Submodule.mem_top
no goals
case refine'_3
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ 0 ∈ I • ⊤
exact Submodule.zero_mem _
case refine'_4
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x y : S
⊢ x ∈ I • ⊤ → y ∈ I • ⊤ → x + y ∈ I • ⊤
case refine'_4
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x : S
hx : x ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
⊢ ∀ (x y : S), x ∈ I • ⊤ → y ∈ I • ⊤ → x + y ∈ I • ⊤
intro x y
no goals
case refine'_4
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
x y : S
⊢ x ∈ I • ⊤ → y ∈ I • ⊤ → x + y ∈ I • ⊤
exact Submodule.add_mem _
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
r : R
hr : r ∈ I
s : S
a✝ : s ∈ ⊤
⊢ a • r • s ∈ I • ⊤
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ ∀ (r : R), r ∈ I → ∀ (n : S), n ∈ ⊤ → a • r • n ∈ I • ⊤
intro r hr s _
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
r : R
hr : r ∈ I
s : S
a✝ : s ∈ ⊤
⊢ r • a • s ∈ I • ⊤
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
r : R
hr : r ∈ I
s : S
a✝ : s ∈ ⊤
⊢ a • r • s ∈ I • ⊤
rw [smul_comm]
no goals
case refine'_5.refine'_1
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
r : R
hr : r ∈ I
s : S
a✝ : s ∈ ⊤
⊢ r • a • s ∈ I • ⊤
exact Submodule.smul_mem_smul hr Submodule.mem_top
case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝¹ : S
hx✝¹ : x✝¹ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x✝ : S
hx✝ : x✝ ∈ I • ⊤
x y : S
hx : a • x ∈ I • ⊤
hy : a • y ∈ I • ⊤
⊢ a • (x + y) ∈ I • ⊤
case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝ : S
hx✝ : x✝ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x : S
hx : x ∈ I • ⊤
⊢ ∀ (x y : S), a • x ∈ I • ⊤ → a • y ∈ I • ⊤ → a • (x + y) ∈ I • ⊤
intro x y hx hy
case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝¹ : S
hx✝¹ : x✝¹ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x✝ : S
hx✝ : x✝ ∈ I • ⊤
x y : S
hx : a • x ∈ I • ⊤
hy : a • y ∈ I • ⊤
⊢ a • x + a • y ∈ I • ⊤
case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝¹ : S
hx✝¹ : x✝¹ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x✝ : S
hx✝ : x✝ ∈ I • ⊤
x y : S
hx : a • x ∈ I • ⊤
hy : a • y ∈ I • ⊤
⊢ a • (x + y) ∈ I • ⊤
rw [smul_add]
no goals
case refine'_5.refine'_2
R✝ : Type u
S✝ : Type v
F : Type ?u.798095
inst✝⁴ : Semiring R✝
inst✝³ : Semiring S✝
rc : RingHomClass F R✝ S✝
f : F
I✝ J : Ideal R✝
K L : Ideal S✝
G : Type ?u.798179
rcg : RingHomClass G S✝ R✝
ι : Sort ?u.798213
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
I : Ideal R
x✝¹ : S
hx✝¹ : x✝¹ ∈ Submodule.restrictScalars R (map (algebraMap R S) I)
a x✝ : S
hx✝ : x✝ ∈ I • ⊤
x y : S
hx : a • x ∈ I • ⊤
hy : a • y ∈ I • ⊤
⊢ a • x + a • y ∈ I • ⊤
exact Submodule.add_mem _ hx hy