-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_sInf {A : Set (Ideal R)} {f : F} (hf : Function.Surjective f) :
    (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
⊢ y ∈ map f (sInf A)

Tactic:
obtain ⟨x, hx⟩ := hf y

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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)

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ ∀ p ∈ A, x ∈ p

Tactic:
intro J hJ

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J

Proof state:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
⊢ y ∈ j

Tactic:
obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy

Result:
case refine_1.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ ∀ I ∈ A, y ∈ map f I

Tactic:
simpa using hy

Result:
no goals

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J

Tactic:
rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩

Result:
case refine_2.intro.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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 ∈ A, f x' ∈ map f I
⊢ x ∈ J

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ x ∈ sInf A

Tactic:
have : ∀ I ∈ A, y ∈ map f I := by simpa using hy

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ x ∈ sInf A

Proof state:
case refine_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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

Tactic:
rw [← hJ.right, ← hx.right]

Result:
case refine_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ x ∈ sInf A

Tactic:
rw [Submodule.mem_sInf]

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ ∀ p ∈ A, x ∈ p

Proof state:
case refine_1.intro.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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

Tactic:
exact mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)

Result:
no goals

Proof state:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ 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)

Tactic:
refine hx ▸ mem_map_of_mem f ?_

Result:
case refine_2.intro
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
⊢ x ∈ sInf A

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)

Tactic:
refine fun h => le_antisymm (le_sInf ?_) ?_

Result:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ ∀ 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
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ sInf (map f '' A) ≤ map f (sInf A)