case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
⊢ ∀ (b : Ideal S), b ∈ map f '' A → map f (sInf A) ≤ b

case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
⊢ (∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)
refine' fun h => le_antisymm (le_sInf _) _
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
⊢ y ∈ j
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
⊢ ∀ (b : Ideal S), b ∈ map f '' A → map f (sInf A) ≤ b
intro j hj y hy
case refine'_1.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
⊢ y ∈ j
case refine'_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
⊢ y ∈ j
cases' (mem_map_iff_of_surjective f hf).1 hy with x hx
case refine'_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ j
case refine'_1.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
⊢ y ∈ j
cases' (Set.mem_image _ _ _).mp hj with J hJ
case refine'_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ ↑f x ∈ map f J
case refine'_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ j
rw [← hJ.right, ← hx.right]
no goals
case refine'_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ ↑f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ ↑f x ∈ map f J
exact mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
⊢ y ∈ map f (sInf A)
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)
intro y hy
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
⊢ y ∈ map f (sInf A)
case refine'_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
⊢ y ∈ map f (sInf A)
cases' hf y with x hx
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
⊢ x ∈ sInf A
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
⊢ y ∈ map f (sInf A)
refine' hx ▸ mem_map_of_mem f _
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
⊢ x ∈ sInf A
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
⊢ x ∈ sInf A
have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
⊢ ∀ (p : Submodule R R), p ∈ A → x ∈ p
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
⊢ x ∈ sInf A
rw [Submodule.mem_sInf]
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
⊢ ∀ (p : Submodule R R), p ∈ A → x ∈ p
intro J hJ
case refine'_2.intro.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
⊢ x ∈ J
case refine'_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
this : ∀ (I : Ideal R), I ∈ A → y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J
rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
case refine'_2.intro.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this✝ : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
this : x - x' ∈ J
⊢ x ∈ J
case refine'_2.intro.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
⊢ x ∈ J
have : x - x' ∈ J := by
  apply h J hJ
  rw [RingHom.mem_ker, map_sub, hx, sub_self]
no goals
case refine'_2.intro.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this✝ : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
this : x - x' ∈ J
⊢ x ∈ J
simpa only [sub_add_cancel] using J.add_mem this hx'
no goals
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : ↑f x = y
⊢ ∀ (I : Ideal R), I ∈ A → y ∈ map f I
simpa using hy
case a
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
⊢ x - x' ∈ RingHom.ker f
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
⊢ x - x' ∈ J
apply h J hJ
no goals
case a
R : Type u_1
S : Type u_2
F : Type u_3
inst✝¹ : Ring R
inst✝ : Ring S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ↑f
h : ∀ (J : Ideal R), J ∈ A → RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : ↑f x' ∈ sInf (map f '' A)
hx : ↑f x = ↑f x'
this : ∀ (I : Ideal R), I ∈ A → ↑f x' ∈ map f I
⊢ x - x' ∈ RingHom.ker f
rw [RingHom.mem_ker, map_sub, hx, sub_self]