Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (generated hI S).carrier = Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
simp only [generated, sInf_carrier_def]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier =
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier =
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
apply le_antisymm
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤
    ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
have h : generatedDpow hI hS ∈ insert ⊤ {J : hI.SubDPIdeal | S ⊆ ↑J.carrier} :=
  by
  apply Set.mem_insert_of_mem
  simp only [Set.mem_setOf_eq, generatedDpow_carrier]
  exact le_generatedDpow hI hS
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier ≤
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
refine' sInf_le_of_le ⟨generatedDpow hI hS, _⟩ (le_refl _)
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ (fun s => ⨅ (_ : s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}), s.carrier) (generatedDpow hI hS) =
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ (fun s => ⨅ (_ : s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}), s.carrier) (generatedDpow hI hS) =
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
simp only [h, ciInf_pos]
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ (generatedDpow hI hS).carrier = Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
h : generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ (generatedDpow hI hS).carrier = Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Tactic:
rfl
State after:
no goals

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ generatedDpow hI hS ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
Tactic:
apply Set.mem_insert_of_mem
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ generatedDpow hI hS ∈ {J | S ⊆ ↑J.carrier}

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ generatedDpow hI hS ∈ {J | S ⊆ ↑J.carrier}
Tactic:
simp only [Set.mem_setOf_eq, generatedDpow_carrier]
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ S ⊆ ↑(Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x})

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ S ⊆ ↑(Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x})
Tactic:
exact le_generatedDpow hI hS
State after:
no goals

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤
    ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier
Tactic:
rw [le_iInf₂_iff]
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ∀ i ∈ insert ⊤ {J | S ⊆ ↑J.carrier},
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ i.carrier

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ ∀ i ∈ insert ⊤ {J | S ⊆ ↑J.carrier},
    Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ i.carrier
Tactic:
rintro J hJ
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ J.carrier

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ J.carrier
Tactic:
refine' generated_dpow_le hI S J _
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ S ⊆ ↑J.carrier

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
⊢ S ⊆ ↑J.carrier
Tactic:
simp only [Set.mem_setOf_eq, Set.mem_insert_iff] at hJ
State after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J = ⊤ ∨ S ⊆ ↑J.carrier
⊢ S ⊆ ↑J.carrier

State before:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJ : J = ⊤ ∨ S ⊆ ↑J.carrier
⊢ S ⊆ ↑J.carrier
Tactic:
cases' hJ with hJI hJS
State after:
case a.inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJI : J = ⊤
⊢ S ⊆ ↑J.carrier

case a.inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJS : S ⊆ ↑J.carrier
⊢ S ⊆ ↑J.carrier

State before:
case a.inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJI : J = ⊤
⊢ S ⊆ ↑J.carrier
Tactic:
rw [hJI]
State after:
case a.inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJI : J = ⊤
⊢ S ⊆ ↑⊤.carrier

State before:
case a.inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJI : J = ⊤
⊢ S ⊆ ↑⊤.carrier
Tactic:
exact hS
State after:
no goals

State before:
case a.inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal
hJS : S ⊆ ↑J.carrier
⊢ S ⊆ ↑J.carrier
Tactic:
exact hJS
State after:
no goals