[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ↑f
⊢ IsAssociatedPrime I M'
[PROOFSTEP]
obtain ⟨x, rfl⟩ := h.2
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M'
[PROOFSTEP]
refine' ⟨h.1, ⟨f x, _⟩⟩
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
⊢ Submodule.annihilator (Submodule.span R {x}) = Submodule.annihilator (Submodule.span R {↑f x})
[PROOFSTEP]
ext r
[GOAL]
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ↑f
x : M
h : IsAssociatedPrime (Submodule.annihilator (Submodule.span R {x})) M
r : R
⊢ r ∈ Submodule.annihilator (Submodule.span R {x}) ↔ r ∈ Submodule.annihilator (Submodule.span R {↑f x})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton, Submodule.mem_annihilator_span_singleton, ← map_smul, ← f.map_zero,
  hf.eq_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ ¬IsAssociatedPrime I M
[PROOFSTEP]
rintro ⟨hI, x, hx⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ False
[PROOFSTEP]
apply hI.ne_top
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
hI : Ideal.IsPrime I
x : M
hx : I = Submodule.annihilator (Submodule.span R {x})
⊢ I = ⊤
[PROOFSTEP]
rwa [Subsingleton.elim x 0, Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at hx
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
have : (R ∙ x).annihilator ≠ ⊤ := by
  rwa [Ne.def, Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
⊢ Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
obtain ⟨P, ⟨l, h₁, y, rfl⟩, h₃⟩ :=
  set_has_maximal_iff_noetherian.mpr H {P | (R ∙ x).annihilator ≤ P ∧ P ≠ ⊤ ∧ ∃ y : M, P = (R ∙ y).annihilator}
    ⟨(R ∙ x).annihilator, rfl.le, this, x, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
⊢ ∃ P, IsAssociatedPrime P M ∧ Submodule.annihilator (Submodule.span R {x}) ≤ P
[PROOFSTEP]
refine' ⟨_, ⟨⟨h₁, _⟩, y, rfl⟩, l⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
⊢ ∀ {x y_1 : R},
    x * y_1 ∈ Submodule.annihilator (Submodule.span R {y}) →
      x ∈ Submodule.annihilator (Submodule.span R {y}) ∨ y_1 ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
intro a b hab
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
⊢ a ∈ Submodule.annihilator (Submodule.span R {y}) ∨ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rw [or_iff_not_imp_left]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
⊢ ¬a ∈ Submodule.annihilator (Submodule.span R {y}) → b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
intro ha
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : a * b ∈ Submodule.annihilator (Submodule.span R {y})
ha : ¬a ∈ Submodule.annihilator (Submodule.span R {y})
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton] at ha hab
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
have H₁ : (R ∙ y).annihilator ≤ (R ∙ a • y).annihilator :=
  by
  intro c hc
  rw [Submodule.mem_annihilator_span_singleton] at hc ⊢
  rw [smul_comm, hc, smul_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
⊢ Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
[PROOFSTEP]
intro c hc
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c ∈ Submodule.annihilator (Submodule.span R {y})
⊢ c ∈ Submodule.annihilator (Submodule.span R {a • y})
[PROOFSTEP]
rw [Submodule.mem_annihilator_span_singleton] at hc ⊢
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
c : R
hc : c • y = 0
⊢ c • a • y = 0
[PROOFSTEP]
rw [smul_comm, hc, smul_zero]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
have H₂ : (Submodule.span R {a • y}).annihilator ≠ ⊤ := by
  rwa [Ne.def, Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
⊢ Submodule.annihilator (Submodule.span R {a • y}) ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot]
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
H : IsNoetherianRing R
x : M
hx : x ≠ 0
this : Submodule.annihilator (Submodule.span R {x}) ≠ ⊤
y : M
h₃ :
  ∀ (I : Submodule R R),
    I ∈
        {P |
          Submodule.annihilator (Submodule.span R {x}) ≤ P ∧
            P ≠ ⊤ ∧ ∃ y, P = Submodule.annihilator (Submodule.span R {y})} →
      ¬Submodule.annihilator (Submodule.span R {y}) < I
l : Submodule.annihilator (Submodule.span R {x}) ≤ Submodule.annihilator (Submodule.span R {y})
h₁ : Submodule.annihilator (Submodule.span R {y}) ≠ ⊤
a b : R
hab : (a * b) • y = 0
ha : ¬a • y = 0
H₁ : Submodule.annihilator (Submodule.span R {y}) ≤ Submodule.annihilator (Submodule.span R {a • y})
H₂ : Submodule.annihilator (Submodule.span R {a • y}) ≠ ⊤
⊢ b ∈ Submodule.annihilator (Submodule.span R {y})
[PROOFSTEP]
rwa [H₁.eq_of_not_lt (h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩), Submodule.mem_annihilator_span_singleton,
  smul_comm, smul_smul]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ associatedPrimes R M = ∅
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
[PROOFSTEP]
simp only [Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ ¬x✝ ∈ associatedPrimes R M
[PROOFSTEP]
apply not_isAssociatedPrime_of_subsingleton
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_ne (0 : M)
[GOAL]
case intro
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right✝ : Submodule.annihilator (Submodule.span R {x}) ≤ P
⊢ Set.Nonempty (associatedPrimes R M)
[PROOFSTEP]
exact ⟨P, hP⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
⊢ Submodule.annihilator ⊤ ≤ I
[PROOFSTEP]
obtain ⟨hI, x, rfl⟩ := h
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : M
hI : Ideal.IsPrime (Submodule.annihilator (Submodule.span R {x}))
⊢ Submodule.annihilator ⊤ ≤ Submodule.annihilator (Submodule.span R {x})
[PROOFSTEP]
exact Submodule.annihilator_mono le_top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
h : IsAssociatedPrime J (R ⧸ I)
⊢ J = Ideal.radical I
[PROOFSTEP]
obtain ⟨hJ, x, e⟩ := h
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ J = Ideal.radical I
[PROOFSTEP]
have : x ≠ 0 := by
  rintro rfl
  apply hJ.1
  rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ False
[PROOFSTEP]
apply hJ.1
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
e : J = Submodule.annihilator (Submodule.span R {0})
⊢ J = ⊤
[PROOFSTEP]
rwa [Submodule.span_singleton_eq_bot.mpr rfl, Submodule.annihilator_bot] at e
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R ⧸ I
e : J = Submodule.annihilator (Submodule.span R {x})
this : x ≠ 0
⊢ J = Ideal.radical I
[PROOFSTEP]
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ J = Ideal.radical I
[PROOFSTEP]
replace e : ∀ {y}, y ∈ J ↔ x * y ∈ I
[GOAL]
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
⊢ ∀ {y : R}, y ∈ J ↔ x * y ∈ I
[PROOFSTEP]
intro y
[GOAL]
case e
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
e : J = Submodule.annihilator (Submodule.span R {↑(Ideal.Quotient.mkₐ R I) x})
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
y : R
⊢ y ∈ J ↔ x * y ∈ I
[PROOFSTEP]
rw [e, Submodule.mem_annihilator_span_singleton, ← map_smul, smul_eq_mul, mul_comm, Ideal.Quotient.mkₐ_eq_mk, ←
  Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J = Ideal.radical I
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ J ≤ Ideal.radical I
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ J
⊢ y ∈ Ideal.radical I
[PROOFSTEP]
exact (hI.2 <| e.mp hy).resolve_left ((Submodule.Quotient.mk_eq_zero I).not.mp this)
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ Ideal.radical I ≤ J
[PROOFSTEP]
rw [hJ.radical_le_iff]
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
⊢ I ≤ J
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.a
R : Type u_1
inst✝⁴ : CommRing R
I J : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hI : Ideal.IsPrimary I
hJ : Ideal.IsPrime J
x : R
this : ↑(Ideal.Quotient.mkₐ R I) x ≠ 0
e : ∀ {y : R}, y ∈ J ↔ x * y ∈ I
y : R
hy : y ∈ I
⊢ y ∈ J
[PROOFSTEP]
exact e.mpr (I.mul_mem_left x hy)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ associatedPrimes R (R ⧸ I) = {Ideal.radical I}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {Ideal.radical I}
[PROOFSTEP]
rw [Set.mem_singleton_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = Ideal.radical I
[PROOFSTEP]
refine' ⟨IsAssociatedPrime.eq_radical hI, _⟩
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J✝ : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
J : Ideal R
⊢ J = Ideal.radical I → J ∈ associatedPrimes R (R ⧸ I)
[PROOFSTEP]
rintro rfl
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
[PROOFSTEP]
haveI : Nontrivial (R ⧸ I) :=
  by
  refine ⟨(Ideal.Quotient.mk I : _) 1, (Ideal.Quotient.mk I : _) 0, ?_⟩
  rw [Ne.def, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
  exact hI.1
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ Nontrivial (R ⧸ I)
[PROOFSTEP]
refine ⟨(Ideal.Quotient.mk I : _) 1, (Ideal.Quotient.mk I : _) 0, ?_⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ↑(Ideal.Quotient.mk I) 1 ≠ ↑(Ideal.Quotient.mk I) 0
[PROOFSTEP]
rw [Ne.def, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
⊢ ¬I = ⊤
[PROOFSTEP]
exact hI.1
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
[PROOFSTEP]
obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsNoetherianRing R
hI : Ideal.IsPrimary I
this : Nontrivial (R ⧸ I)
a : Ideal R
ha : a ∈ associatedPrimes R (R ⧸ I)
⊢ Ideal.radical I ∈ associatedPrimes R (R ⧸ I)
[PROOFSTEP]
exact ha.eq_radical hI ▸ ha


[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(constantCoeff R) (invUnitsSub u) = 1 /ₚ u
[PROOFSTEP]
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ invUnitsSub u * X = invUnitsSub u * ↑(C R) ↑u - 1
[PROOFSTEP]
ext (_ | n)
[GOAL]
case h.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(coeff R Nat.zero) (invUnitsSub u * X) = ↑(coeff R Nat.zero) (invUnitsSub u * ↑(C R) ↑u - 1)
[PROOFSTEP]
simp
[GOAL]
case h.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
n : ℕ
⊢ ↑(coeff R (Nat.succ n)) (invUnitsSub u * X) = ↑(coeff R (Nat.succ n)) (invUnitsSub u * ↑(C R) ↑u - 1)
[PROOFSTEP]
simp [n.succ_ne_zero, pow_succ]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ invUnitsSub u * (↑(C R) ↑u - X) = 1
[PROOFSTEP]
simp [mul_sub, sub_sub_cancel]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ ↑(map f) (invUnitsSub u) = invUnitsSub (↑(Units.map ↑f) u)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (invUnitsSub u)) = ↑(coeff S n✝) (invUnitsSub (↑(Units.map ↑f) u))
[PROOFSTEP]
simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑f ↑(u ^ (n✝ + 1))⁻¹ = ↑(↑(Units.map ↑f) (u ^ (n✝ + 1)))⁻¹
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(constantCoeff A) (exp A) = 1
[PROOFSTEP]
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(algebraMap ℚ A) (1 / ↑0!) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit0 n)) (sin A) = 0
[PROOFSTEP]
rw [sin, coeff_mk, if_pos (even_bit0 n)]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit1 n)) (sin A) = (-1) ^ n * ↑(coeff A (bit1 n)) (exp A)
[PROOFSTEP]
rw [sin, coeff_mk, if_neg n.not_even_bit1, Nat.bit1_div_two, ← mul_one_div, map_mul, map_pow, map_neg, map_one,
  coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit0 n)) (cos A) = (-1) ^ n * ↑(coeff A (bit0 n)) (exp A)
[PROOFSTEP]
rw [cos, coeff_mk, if_pos (even_bit0 n), Nat.bit0_div_two, ← mul_one_div, map_mul, map_pow, map_neg, map_one, coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit1 n)) (cos A) = 0
[PROOFSTEP]
rw [cos, coeff_mk, if_neg n.not_even_bit1]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (exp A) = exp A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (exp A)) = ↑(coeff A' n✝) (exp A')
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (sin A) = sin A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (sin A)) = ↑(coeff A' n✝) (sin A')
[PROOFSTEP]
simp [sin, apply_ite f]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (cos A) = cos A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (cos A)) = ↑(coeff A' n✝) (cos A')
[PROOFSTEP]
simp [cos, apply_ite f]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
⊢ ↑(rescale a) (exp A) * ↑(rescale b) (exp A) = ↑(rescale (a + b)) (exp A)
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ↑(coeff A n) (↑(rescale a) (exp A) * ↑(rescale b) (exp A)) = ↑(coeff A n) (↑(rescale (a + b)) (exp A))
[PROOFSTEP]
simp only [coeff_mul, exp, rescale, coeff_mk, MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, factorial,
  Nat.sum_antidiagonal_eq_sum_range_succ_mk, add_pow, sum_mul]
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ (Finset.sum (Finset.range (succ n)) fun x =>
      a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!))) =
    Finset.sum (Finset.range (n + 1)) fun x => a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (succ n) →
      a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
        a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rintro x hx
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
suffices
  a ^ x * b ^ (n - x) * (algebraMap ℚ A (1 / ↑x.factorial) * algebraMap ℚ A (1 / ↑(n - x).factorial)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n.factorial))
  by convert this using 1 <;> ring
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!))
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
ring
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = ↑(algebraMap ℚ A) (↑(Nat.choose n x) * (1 / ↑n !))
[PROOFSTEP]
refine' RingHom.congr_arg _ _
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ 1 / ↑x ! * (1 / ↑(n - x)!) = ↑(Nat.choose n x) * (1 / ↑n !)
[PROOFSTEP]
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ 1 / (↑x ! * ↑(n - x)!) = ↑(Nat.choose n x) / ↑n !
[PROOFSTEP]
symm
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(Nat.choose n x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)
[PROOFSTEP]
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / (↑x ! * ↑(n - x)!)
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / ↑(x ! * (n - x)!)
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
rw [cast_div_charZero]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ! * (n - x)! ∣ n !
[PROOFSTEP]
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
[PROOFSTEP]
apply mem_range_succ_iff.1 hx
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
rintro h
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
h : ↑n ! = 0
⊢ False
[PROOFSTEP]
apply factorial_ne_zero n
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
h : ↑n ! = 0
⊢ n ! = 0
[PROOFSTEP]
rw [cast_eq_zero.1 h]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A * ↑evalNegHom (exp A) = 1
[PROOFSTEP]
convert exp_mul_exp_eq_exp_add (1 : A) (-1)
[GOAL]
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A = ↑(rescale 1) (exp A)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = ↑(rescale (1 + -1)) (exp A)
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = ↑(rescale ↑k) (exp A)
[PROOFSTEP]
induction' k with k h
[GOAL]
case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ zero = ↑(rescale ↑zero) (exp A)
[PROOFSTEP]
simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero, zero_eq, pow_zero (exp A),
  coe_comp]
[GOAL]
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = ↑(rescale ↑k) (exp A)
⊢ exp A ^ succ k = ↑(rescale ↑(succ k)) (exp A)
[PROOFSTEP]
simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one, id_apply, rescale_one] using
  pow_succ' (exp A) k
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (Finset.sum (Finset.range n) fun k => exp A ^ k) =
    mk fun p => Finset.sum (Finset.range n) fun k => ↑(k ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹
[PROOFSTEP]
simp only [exp_pow_eq_rescale_exp, rescale]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (Finset.sum (Finset.range n) fun x =>
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                    map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (f g : PowerSeries A),
                      OneHom.toFun
                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                          (f * g) =
                        OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            f *
                          OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            g) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (f g : PowerSeries A),
                              OneHom.toFun
                                  { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                    map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                  (f * g) =
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    f *
                                  OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    g) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x_1 y : PowerSeries A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : PowerSeries A),
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      g) })
                      (x_1 + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        x_1 +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        y) }
        (exp A)) =
    mk fun p => Finset.sum (Finset.range n) fun x => ↑(x ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ ↑(coeff A n✝)
      (Finset.sum (Finset.range n) fun x =>
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (f g : PowerSeries A),
                        OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            (f * g) =
                          OneHom.toFun
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                              f *
                            OneHom.toFun
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                              g) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : PowerSeries A),
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      g) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x_1 y : PowerSeries A),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        (x_1 + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                  map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : PowerSeries A),
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          g) })
                          x_1 +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                  map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : PowerSeries A),
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          g) })
                          y) }
          (exp A)) =
    ↑(coeff A n✝) (mk fun p => Finset.sum (Finset.range n) fun x => ↑(x ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹)
[PROOFSTEP]
simp only [one_div, coeff_mk, cast_pow, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, factorial,
  LinearMap.map_sum]


[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
suffices
  ∃ m ∈ {p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p},
    OrderDual.toDual J ≤ m ∧ ∀ z ∈ {p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p}, m ≤ z → z = m
  by
  obtain ⟨p, h₁, h₂, h₃⟩ := this
  simp_rw [← @eq_comm _ p] at h₃
  exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
this :
  ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
obtain ⟨p, h₁, h₂, h₃⟩ := this
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → z = p
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
simp_rw [← @eq_comm _ p] at h₃
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → p = z
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
[PROOFSTEP]
exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
[PROOFSTEP]
apply zorn_nonempty_partialOrder₀
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
case hxs
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
[PROOFSTEP]
swap
[GOAL]
case hxs
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
[PROOFSTEP]
refine' ⟨show J.IsPrime by infer_instance, e⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ IsPrime J
[PROOFSTEP]
infer_instance
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
[PROOFSTEP]
rintro (c : Set (Ideal R)) hc hc' J' hJ'
[GOAL]
case ih
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
[PROOFSTEP]
refine' ⟨OrderDual.toDual (sInf c), ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩
[GOAL]
case ih.refine'_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ ↑OrderDual.ofDual (↑OrderDual.toDual (sInf c))
[PROOFSTEP]
rw [OrderDual.ofDual_toDual, le_sInf_iff]
[GOAL]
case ih.refine'_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (b : Ideal R), b ∈ c → I ≤ b
[PROOFSTEP]
exact fun _ hx => (hc hx).2
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ↑OrderDual.toDual (sInf c)
[PROOFSTEP]
rintro z hz
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ ↑OrderDual.toDual (sInf c)
[PROOFSTEP]
rw [OrderDual.le_toDual]
[GOAL]
case ih.refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ ↑OrderDual.ofDual z
[PROOFSTEP]
exact sInf_le hz
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes (radical I) = Ideal.minimalPrimes I
[PROOFSTEP]
rw [Ideal.minimalPrimes, Ideal.minimalPrimes]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} =
    minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
ext p
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} ↔
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case h.refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p} →
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
rintro ⟨⟨a, ha⟩, b⟩
[GOAL]
case h.refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p} →
    p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
[PROOFSTEP]
rintro ⟨⟨a, ha⟩, b⟩
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : radical I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
[PROOFSTEP]
simp only [Set.mem_setOf_eq, and_imp] at *
[GOAL]
case h.refine'_1.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : radical I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
[PROOFSTEP]
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ p ∈ minimals (fun x x_1 => x ≤ x_1) {p | IsPrime p ∧ radical I ≤ p}
[PROOFSTEP]
refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
b : ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
a : IsPrime p
ha : I ≤ p
⊢ ∀ ⦃b : Ideal R⦄, b ∈ {p | IsPrime p ∧ radical I ≤ p} → (fun x x_1 => x ≤ x_1) b p → (fun x x_1 => x ≤ x_1) p b
[PROOFSTEP]
simp only [Set.mem_setOf_eq, and_imp] at *
[GOAL]
case h.refine'_2.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J p : Ideal R
a : IsPrime p
ha : I ≤ p
b : ∀ ⦃b : Ideal R⦄, IsPrime b → I ≤ b → b ≤ p → p ≤ b
⊢ ∀ ⦃b : Ideal R⦄, IsPrime b → radical I ≤ b → b ≤ p → p ≤ b
[PROOFSTEP]
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = radical I
[PROOFSTEP]
rw [I.radical_eq_sInf]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) = sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf (Ideal.minimalPrimes I) ≤ sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : x ∈ sInf (Ideal.minimalPrimes I)
⊢ x ∈ sInf {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
rw [Ideal.mem_sInf] at hx ⊢
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsPrime J} → x ∈ I_1
[PROOFSTEP]
rintro J ⟨e, hJ⟩
[GOAL]
case a.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
⊢ x ∈ J
[PROOFSTEP]
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
[GOAL]
case a.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ Ideal.minimalPrimes I → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : IsPrime J
p : Ideal R
hp : p ∈ Ideal.minimalPrimes I
hp' : p ≤ J
⊢ x ∈ J
[PROOFSTEP]
exact hp' (hx hp)
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ sInf {J | I ≤ J ∧ IsPrime J} ≤ sInf (Ideal.minimalPrimes I)
[PROOFSTEP]
apply sInf_le_sInf _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I ⊆ {J | I ≤ J ∧ IsPrime J}
[PROOFSTEP]
intro I hI
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J I : Ideal R
hI : I ∈ Ideal.minimalPrimes I✝
⊢ I ∈ {J | I✝ ≤ J ∧ IsPrime J}
[PROOFSTEP]
exact hI.1.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
have := H.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
have : Nontrivial (Localization (Submonoid.map f p.primeCompl)) :=
  by
  refine' ⟨⟨1, 0, _⟩⟩
  convert
    (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p)
          (Localization <| p.primeCompl.map f) hf).ne
      one_ne_zero
  · rw [map_one]
  · rw [map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ Nontrivial (Localization (Submonoid.map f (primeCompl p)))
[PROOFSTEP]
refine' ⟨⟨1, 0, _⟩⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 ≠ 0
[PROOFSTEP]
convert
  (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p) (Localization <| p.primeCompl.map f)
        hf).ne
    one_ne_zero
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 1 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      1
[PROOFSTEP]
rw [map_one]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this : IsPrime p
⊢ 0 =
    ↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      0
[PROOFSTEP]
rw [map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl))
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ ∃ p', IsPrime p' ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap f (comap (algebraMap S (Localization (Submonoid.map f (primeCompl p)))) M) = p
[PROOFSTEP]
rw [Ideal.comap_comap, ←
  @IsLocalization.map_comp _ _ _ _ _ _ _ _ Localization.isLocalization _ _ _ _ p.primeCompl.le_comap_map _
    Localization.isLocalization,
  ← Ideal.comap_comap]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
[PROOFSTEP]
suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝¹ : IsPrime p
this✝ : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
this : ?m.48761 ≤ p
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) =
    p
[PROOFSTEP]
exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this)
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
⊢ comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M) ≤
    p
[PROOFSTEP]
intro x hx
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
⊢ x ∈ p
[PROOFSTEP]
by_contra h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ False
[PROOFSTEP]
apply hM.ne_top
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ M = ⊤
[PROOFSTEP]
apply M.eq_top_of_isUnit_mem hx
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit
    (↑(IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
      (↑(algebraMap R (Localization (primeCompl p))) x))
[PROOFSTEP]
apply IsUnit.map
[GOAL]
case intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Injective ↑f
p : Ideal R
H : p ∈ minimalPrimes R
this✝ : IsPrime p
this : Nontrivial (Localization (Submonoid.map f (primeCompl p)))
M : Ideal (Localization (Submonoid.map f (primeCompl p)))
hM : IsMaximal M
x : R
hx :
  x ∈
    comap (algebraMap R (Localization (primeCompl p)))
      (comap
        (IsLocalization.map (Localization (Submonoid.map f (primeCompl p))) f
          (_ : primeCompl p ≤ Submonoid.comap f (Submonoid.map f (primeCompl p))))
        M)
h : ¬x ∈ p
⊢ IsUnit (↑(algebraMap R (Localization (primeCompl p))) x)
[PROOFSTEP]
apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have := H.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
let f' := (Ideal.Quotient.mk I).comp f
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have e : RingHom.ker f' = I.comap f := by
  ext1
  exact Submodule.Quotient.mk_eq_zero _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
⊢ RingHom.ker f' = comap f I
[PROOFSTEP]
ext1
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
x✝ : R
⊢ x✝ ∈ RingHom.ker f' ↔ x✝ ∈ comap f I
[PROOFSTEP]
exact Submodule.Quotient.mk_eq_zero _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p :=
  by
  rw [Ideal.mk_ker, e]
  exact H.1.2
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
[PROOFSTEP]
rw [Ideal.mk_ker, e]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
⊢ comap f I ≤ p
[PROOFSTEP]
exact H.1.2
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
suffices _
  by
  have ⟨p', hp₁, hp₂⟩ :=
    Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective (RingHom.kerLift_injective f')
      (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this
  refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩
  · exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)
  · convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
    rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') Ideal.Quotient.mk_surjective, eq_comm,
      sup_eq_left]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : ?m.53321
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
have ⟨p', hp₁, hp₂⟩ :=
  Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective (RingHom.kerLift_injective f')
    (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ ∃ p', IsPrime p' ∧ I ≤ p' ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ I ≤ comap (Quotient.mk I) p'
[PROOFSTEP]
exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ comap f (comap (Quotient.mk I) p') = p
[PROOFSTEP]
convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝¹ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this✝ : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
this : map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
p' : Ideal (S ⧸ I)
hp₁ : IsPrime p'
hp₂ : comap (RingHom.kerLift f') p' = map (Quotient.mk (RingHom.ker f')) p
⊢ p = comap (Quotient.mk (RingHom.ker f')) (map (Quotient.mk (RingHom.ker f')) p)
[PROOFSTEP]
rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') Ideal.Quotient.mk_surjective, eq_comm,
  sup_eq_left]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f')
[PROOFSTEP]
refine' ⟨⟨_, bot_le⟩, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ IsPrime (map (Quotient.mk (RingHom.ker f')) p)
[PROOFSTEP]
apply Ideal.map_isPrime_of_surjective _ this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker f'))
[PROOFSTEP]
exact Ideal.Quotient.mk_surjective
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
⊢ ∀ ⦃b : Ideal (R ⧸ RingHom.ker f')⦄,
    b ∈ {p | IsPrime p ∧ ⊥ ≤ p} →
      (fun x x_1 => x ≤ x_1) b (map (Quotient.mk (RingHom.ker f')) p) →
        (fun x x_1 => x ≤ x_1) (map (Quotient.mk (RingHom.ker f')) p) b
[PROOFSTEP]
rintro q ⟨hq, -⟩ hq'
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤ q
[PROOFSTEP]
rw [←
  Ideal.map_comap_of_surjective (Ideal.Quotient.mk (RingHom.ker ((Ideal.Quotient.mk I).comp f)))
    Ideal.Quotient.mk_surjective q]
[GOAL]
case refine'_2.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ map (Quotient.mk (RingHom.ker f')) p ≤
    map (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
      (comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q)
[PROOFSTEP]
apply Ideal.map_mono
[GOAL]
case refine'_2.intro.h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ≤ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q
[PROOFSTEP]
apply H.2
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ∈ {p | IsPrime p ∧ comap f I ≤ p}
[PROOFSTEP]
refine' ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) q ≤ p
[PROOFSTEP]
refine' (Ideal.comap_mono hq').trans _
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) (map (Quotient.mk (RingHom.ker f')) p) ≤ p
[PROOFSTEP]
rw [Ideal.comap_map_of_surjective]
[GOAL]
case refine'_2.intro.h.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ p ⊔ comap (Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f))) ⊥ ≤ p
case refine'_2.intro.h.a.hf
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
this✝ : IsPrime p
f' : R →+* S ⧸ I := RingHom.comp (Quotient.mk I) f
e : RingHom.ker f' = comap f I
this : RingHom.ker (Quotient.mk (RingHom.ker f')) ≤ p
q : Ideal (R ⧸ RingHom.ker f')
hq : IsPrime q
hq' : q ≤ map (Quotient.mk (RingHom.ker f')) p
⊢ Function.Surjective ↑(Quotient.mk (RingHom.ker (RingHom.comp (Quotient.mk I) f)))
[PROOFSTEP]
exacts [sup_le rfl.le this, Ideal.Quotient.mk_surjective]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ ∃ p', p' ∈ Ideal.minimalPrimes I ∧ comap f p' = p
[PROOFSTEP]
refine' ⟨q, hq, Eq.symm _⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
⊢ p = comap f q
[PROOFSTEP]
have := hq.1.1
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this : IsPrime q
⊢ p = comap f q
[PROOFSTEP]
have := (Ideal.comap_mono hq').trans_eq h₃
[GOAL]
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ Ideal.minimalPrimes (comap f I)
p' : Ideal S
h₁ : IsPrime p'
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ Ideal.minimalPrimes I
hq' : q ≤ p'
this✝ : IsPrime q
this : comap f q ≤ p
⊢ p = comap f q
[PROOFSTEP]
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
have := h.1.1
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
⊢ ∀ ⦃b : Ideal R⦄,
    b ∈ {p | IsPrime p ∧ comap f I ≤ p} → (fun x x_1 => x ≤ x_1) b (comap f J) → (fun x x_1 => x ≤ x_1) (comap f J) b
[PROOFSTEP]
rintro K ⟨hK, e₁⟩ e₂
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K
[PROOFSTEP]
have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
[PROOFSTEP]
rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)
[PROOFSTEP]
apply Ideal.comap_mono _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
[PROOFSTEP]
apply h.2 _ _
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ∈ {p | IsPrime p ∧ I ≤ p}
[PROOFSTEP]
exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
h : J ∈ Ideal.minimalPrimes I
this✝ : IsPrime J
K : Ideal R
hK : IsPrime K
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J
[PROOFSTEP]
exact Ideal.map_le_of_le_comap e₂
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
⊢ Ideal.minimalPrimes (comap f I) = comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) ↔ J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes (comap f I) → J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
intro H
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
H : J ∈ Ideal.minimalPrimes (comap f I)
⊢ J ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
[GOAL]
case h.mp.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I p : Ideal S
h : p ∈ Ideal.minimalPrimes I
H : comap f p ∈ Ideal.minimalPrimes (comap f I)
⊢ comap f p ∈ comap f '' Ideal.minimalPrimes I
[PROOFSTEP]
exact ⟨p, h, rfl⟩
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' Ideal.minimalPrimes I → J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
rintro ⟨J, hJ, rfl⟩
[GOAL]
case h.mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I✝ J✝ : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
I J : Ideal S
hJ : J ∈ Ideal.minimalPrimes I
⊢ comap f J ∈ Ideal.minimalPrimes (comap f I)
[PROOFSTEP]
exact Ideal.mimimal_primes_comap_of_surjective hf hJ
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
⊢ Ideal.minimalPrimes I = comap (Quotient.mk I) '' minimalPrimes (R ⧸ I)
[PROOFSTEP]
rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, ←
  RingHom.ker_eq_comap_bot, Ideal.mk_ker]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ Ideal.minimalPrimes I = {radical I}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {radical I}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {radical I}
[PROOFSTEP]
exact fun H =>
  let e := H.1.1.radical_le_iff.mpr H.1.2
  (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J✝ : Ideal R
hI : IsPrimary I
J : Ideal R
⊢ J ∈ {radical I} → J ∈ Ideal.minimalPrimes I
[PROOFSTEP]
rintro (rfl : J = I.radical)
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hI : IsPrimary I
⊢ radical I ∈ Ideal.minimalPrimes I
[PROOFSTEP]
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime I
⊢ Ideal.minimalPrimes I = {I}
[PROOFSTEP]
ext J
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {I}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {I}
[PROOFSTEP]
exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ {I} → J ∈ Ideal.minimalPrimes I
[PROOFSTEP]
rintro (rfl : J = I)
[GOAL]
case h.mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
J✝ J : Ideal R
inst✝ : IsPrime J
⊢ J ∈ Ideal.minimalPrimes J
[PROOFSTEP]
refine' ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩