internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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}
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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 _)
Proof 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}
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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]
Proof 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}
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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}
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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]
Proof 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})
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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]
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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 _
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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]
Proof 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
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.SubDPIdeal.generated_carrier_eq
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ hI.isSubDPIdeal (RingHom.ker f ⊓ I)
Tactic:
rw [isSubDPIdeal_inf_iff]
Proof state after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
simp only [isDPMorphism] at hf
Proof state after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
intro n a b ha hb
Proof state after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
simp only [RingHom.sub_mem_ker_iff]
Proof state after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → f (hI.dpow n a) = f (hI.dpow n b)
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → f (hI.dpow n a) = f (hI.dpow n b)
Tactic:
rw [← hf.2 n a ha, ← hf.2 n b hb]
Proof state after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)
Theorem: DividedPowers.isSubDPIdeal_ker
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)
Tactic:
exact congr_arg _
Proof state after:
no goals
Theorem: DividedPowers.mem_dpEqualizer_iff
Proof state before:
A✝ : Type ?u.85550
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
⊢ x ∈ hI.dpEqualizer hI' ↔ x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
Tactic:
simp only [dpEqualizer, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_setOf_eq]
Proof state after:
no goals
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI.isSubDPIdeal (hI.dpEqualizer hI')
Tactic:
apply isSubDPIdeal.mk
Proof state after:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI.dpEqualizer hI' ≤ I

case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI.dpow n j ∈ hI.dpEqualizer hI'
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI.dpEqualizer hI' ≤ I
Tactic:
intro x hx
Proof state after:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I
Tactic:
rw [mem_dpEqualizer_iff] at hx
Proof state after:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case isSubIdeal
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I
Tactic:
exact hx.1
Proof state after:
no goals
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI.dpow n j ∈ hI.dpEqualizer hI'
Tactic:
intro n hn x hx
Proof state after:
case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ hI.dpow n x ∈ hI.dpEqualizer hI'
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ hI.dpow n x ∈ hI.dpEqualizer hI'
Tactic:
rw [mem_dpEqualizer_iff] at hx ⊢
Proof state after:
case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI.dpow n x ∈ I ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI.dpow n x ∈ I ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Tactic:
constructor
Proof state after:
case dpow_mem.left
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI.dpow n x ∈ I

case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem.left
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI.dpow n x ∈ I

case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Tactic:
apply hI.dpow_mem hn hx.1
Proof state after:
case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI.dpow n x) = hI'.dpow n_1 (hI.dpow n x)
Tactic:
intro m
Proof state after:
case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
m : ℕ
⊢ hI.dpow m (hI.dpow n x) = hI'.dpow m (hI.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_left
Proof state before:
case dpow_mem.right
A✝ : Type ?u.86677
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
m : ℕ
⊢ hI.dpow m (hI.dpow n x) = hI'.dpow m (hI.dpow n x)
Tactic:
rw [hI.dpow_comp m hn hx.1, hx.2, hx.2, hI'.dpow_comp m hn hx.1]
Proof state after:
no goals
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI'.isSubDPIdeal (hI.dpEqualizer hI')
Tactic:
apply isSubDPIdeal.mk
Proof state after:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI.dpEqualizer hI' ≤ I

case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI'.dpow n j ∈ hI.dpEqualizer hI'
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ hI.dpEqualizer hI' ≤ I
Tactic:
intro x hx
Proof state after:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I
Tactic:
rw [mem_dpEqualizer_iff] at hx
Proof state after:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case isSubIdeal
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I
Tactic:
exact hx.1
Proof state after:
no goals
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI'.dpow n j ∈ hI.dpEqualizer hI'
Tactic:
intro n hn x hx
Proof state after:
case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ hI'.dpow n x ∈ hI.dpEqualizer hI'
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ hI'.dpow n x ∈ hI.dpEqualizer hI'
Tactic:
rw [mem_dpEqualizer_iff] at hx ⊢
Proof state after:
case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI'.dpow n x ∈ I ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI'.dpow n x ∈ I ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Tactic:
constructor
Proof state after:
case dpow_mem.left
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI'.dpow n x ∈ I

case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)