awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m : ℕ
hm : m ≠ 0
add : Membership.mem (γ := Ideal A) (span S) (∑ k ∈ range (m + 1), hI.dpow k x * hI.dpow (m - k) y)
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m (x + y))

Tactic:
rw [hI.dpow_add' (hSI hxI) (hSI hyI)]

Premises used: DividedPowers.dpow_add'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m : ℕ
hm : m ≠ 0
add : ∀ c ∈ range (m + 1), Membership.mem (γ := Submodule A A) (span S) (hI.dpow c x * hI.dpow (m - c) y)
⊢ Membership.mem (γ := Ideal A) (span S) (∑ k ∈ range (m + 1), hI.dpow k x * hI.dpow (m - k) y)

Tactic:
apply Submodule.sum_mem (span S)

Premises used: Submodule.sum_mem, Ideal.span
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
add : m ∈ range (m_1 + 1) → Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
⊢ m ∈ range (m_1 + 1) → Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
_
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
h : m ∈ range (m_1 + 1)
pos : ∀ (hm0 : m = 0), Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
neg : ∀ (hm0 : ¬m = 0), Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
h : m ∈ range (m_1 + 1)
hm0 : m = 0
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
hm0 ▸ mul_mem_left (span S) _ (hy _ hm)

Premises used: Eq.rec, Ideal.span, Ideal.mul_mem_left, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
h : m ∈ range (m_1 + 1)
hm0 : m = 0
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
exact hm0 ▸ mul_mem_left (span S) _ (hy _ hm)
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
h : m ∈ range (m_1 + 1)
hm0 : ¬m = 0
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
mul_mem_right _ (span S) (hx _ hm0)

Premises used: Set.Mem, Ideal.mul_mem_right, Ideal.span
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z x y : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)
m_1 : ℕ
hm : m_1 ≠ 0
m : ℕ
h : m ∈ range (m_1 + 1)
hm0 : ¬m = 0
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)

Tactic:
exact mul_mem_right _ (span S) (hx _ hm0)

Premises used: Ideal.mul_mem_right, Ideal.span
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z a x : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
m : ℕ
hm : m ≠ 0
smul : Membership.mem (γ := Ideal A) (span S) (a ^ m * hI.dpow m x)
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m (a • x))

Tactic:
rw [smul_eq_mul, hI.dpow_mul (hSI hxI)]

Premises used: DividedPowers.dpow_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z a x : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) (a ^ m * hI.dpow m x)

Tactic:
mul_mem_left (span S) (a ^ m) (hx m hm)

Premises used: HPow.hPow, Ideal.span, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
z a x : A
hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x
hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) (a ^ m * hI.dpow m x)

Tactic:
exact mul_mem_left (span S) (a ^ m) (hx m hm)

Premises used: HPow.hPow, Ideal.span, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ (↑I : Set A)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
m : ℕ
hm : m ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span S) z
mem : ∀ (x : A) (h : x ∈ S) (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
zero : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m 0)
add :
  ∀ (x y : A) (hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x)
    (hyI : Membership.mem (γ := Submodule A A) (Submodule.span A S) y)
    (hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x))
    (hy : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m y)) (m : ℕ) (hm : m ≠ 0),
    Membership.mem (γ := Ideal A) (span S) (hI.dpow m (x + y))
smul :
  ∀ (a x : A) (hxI : Membership.mem (γ := Submodule A A) (Submodule.span A S) x)
    (hx : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)) (m : ℕ) (hm : m ≠ 0),
    Membership.mem (γ := Ideal A) (span S) (hI.dpow m (a • x))
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m z)

Tactic:
induction hz using Submodule.span_induction generalizing m hm with
    | mem x h => exact hhI hm x h
    | zero =>
        rw [hI.dpow_eval_zero hm]
        exact (span S).zero_mem
    | add x y hxI hyI hx hy =>
        rw [hI.dpow_add' (hSI hxI) (hSI hyI)]
        apply Submodule.sum_mem (span S)
        intro m _
        by_cases hm0 : m = 0
        · exact hm0 ▸ mul_mem_left (span S) _ (hy _ hm)
        · exact mul_mem_right _ (span S) (hx _ hm0)
    | smul a x hxI hx =>
        rw [smul_eq_mul, hI.dpow_mul (hSI hxI)]
        exact mul_mem_left (span S) (a ^ m) (hx m hm)

Premises used: Submodule.sum_mem, DividedPowers.dpow_eval_zero, Ideal.zero_mem, Subtype.mem, Ideal.span, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
rw :
  ∀ {n : ℕ},
    n ≠ 0 →
      ∀ s ∈ (↑J : Set A) ∪ (↑K : Set A),
        Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n s)
⊢ hI.IsSubDPIdeal (J ⊔ K)

Tactic:
rw [← J.span_eq, ← K.span_eq, ← span_union,
    span_isSubDPIdeal_iff (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)]

Premises used: Iff.mpr, Set.union_subset_iff, Ideal.span_eq, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.span_isSubDPIdeal_iff, And.intro, Ideal.span_union
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ (↑J : Set A) ∪ (↑K : Set A)
inl : ∀ (ha : a ∈ (↑J : Set A)), Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)
inr : ∀ (ha : a ∈ (↑K : Set A)), Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)
⊢ Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)

Tactic:
rcases ha with ha | ha
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ (↑J : Set A)
⊢ Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)

Tactic:
span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))

Premises used: Ideal.subset_span, Set.Mem, DividedPowers.IsSubDPIdeal.dpow_mem, Set.subset_union_left, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ (↑J : Set A)
⊢ Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)

Tactic:
exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))

Premises used: Ideal.subset_span, DividedPowers.IsSubDPIdeal.dpow_mem, Set.subset_union_left, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ (↑K : Set A)
⊢ Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)

Tactic:
span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))

Premises used: Ideal.subset_span, Set.Mem, Set.subset_union_right, DividedPowers.IsSubDPIdeal.dpow_mem, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ (↑K : Set A)
⊢ Membership.mem (γ := Ideal A) (span ((↑J : Set A) ∪ (↑K : Set A))) (hI.dpow n a)

Tactic:
exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))

Premises used: Ideal.subset_span, Set.subset_union_right, DividedPowers.IsSubDPIdeal.dpow_mem, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
rw :
  ∀ {n : ℕ},
    n ≠ 0 →
      ∀ (s : A),
        Membership.mem (γ := Set A) (⋃ (i : ι), (↑(J i) : Set A)) s →
          Membership.mem (γ := Ideal A) (span (⋃ (i : ι), (↑(J i) : Set A))) (hI.dpow n s)
⊢ hI.IsSubDPIdeal (iSup J)

Tactic:
rw [iSup_eq_span, span_isSubDPIdeal_iff (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)]

Premises used: Iff.mpr, Set.iUnion_subset_iff, Ideal.iSup_eq_span, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.span_isSubDPIdeal_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
simp_rw :
  ∀ {n : ℕ},
    n ≠ 0 →
      ∀ (s : A),
        (∃ (i : ι), s ∈ (↑(J i) : Set A)) →
          Membership.mem (γ := Ideal A) (span (⋃ (i : ι), (↑(J i) : Set A))) (hI.dpow n s)
⊢ ∀ {n : ℕ},
    n ≠ 0 →
      ∀ (s : A),
        Membership.mem (γ := Set A) (⋃ (i : ι), (↑(J i) : Set A)) s →
          Membership.mem (γ := Ideal A) (span (⋃ (i : ι), (↑(J i) : Set A))) (hI.dpow n s)

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ (↑(J i) : Set A)
⊢ Membership.mem (γ := Ideal A) (span (⋃ (i : ι), (↑(J i) : Set A))) (hI.dpow n a)

Tactic:
span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha))

Premises used: Ideal.subset_span, Set.Mem, DividedPowers.IsSubDPIdeal.dpow_mem, Set.subset_iUnion, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
n : ℕ
hn : n ≠ 0
a : A
i : ι
ha : a ∈ (↑(J i) : Set A)
⊢ Membership.mem (γ := Ideal A) (span (⋃ (i : ι), (↑(J i) : Set A))) (hI.dpow n a)

Tactic:
exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha))

Premises used: Ideal.subset_span, Set.subset_iUnion, Ideal.span_mono
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : Nonempty ι
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ (i : ι), J i)

Tactic:
⟨fun _ hx ↦ hx.1, ?_⟩

Premises used: And.left, DividedPowers.IsSubDPIdeal.mk
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : Nonempty ι
inr : ∀ (n : ℕ), n ≠ 0 → ∀ {j : A}, j ∈ I ⊓ ⨅ (i : ι), J i → hI.dpow n j ∈ I ⊓ ⨅ (i : ι), J i
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ (i : ι), J i)

Tactic:
refine ⟨fun _ hx ↦ hx.1, ?_⟩
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : Nonempty ι
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ⊓ ⨅ (i : ι), J i
inr : ∀ (hx : x ∈ I ∧ ∀ (i : ι), x ∈ J i), hI.dpow n x ∈ I ∧ ∀ (i : ι), hI.dpow n x ∈ J i
⊢ hI.dpow n x ∈ I ⊓ ⨅ (i : ι), J i

Tactic:
simp only [Ideal.mem_inf, mem_iInf] at hx ⊢

Premises used: Ideal.mem_iInf, Ideal.mem_inf
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : Nonempty ι
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (i : ι), x ∈ J i
⊢ hI.dpow n x ∈ I ∧ ∀ (i : ι), hI.dpow n x ∈ J i

Tactic:
⟨hI.dpow_mem hn hx.1, fun i ↦  IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩

Premises used: DividedPowers.dpow_mem, DividedPowers.IsSubDPIdeal.dpow_mem, And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : Nonempty ι
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (i : ι), x ∈ J i
⊢ hI.dpow n x ∈ I ∧ ∀ (i : ι), hI.dpow n x ∈ J i

Tactic:
exact ⟨hI.dpow_mem hn hx.1, fun i ↦  IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : IsEmpty ι
inl : hI.IsSubDPIdeal I
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ (i : ι), J i)

Tactic:
simp only [iInf_of_empty, le_top, inf_of_le_left]

Premises used: iInf_of_empty, inf_of_le_left, le_top
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : IsEmpty ι
⊢ hI.IsSubDPIdeal I

Tactic:
IsSubDPIdeal.self hI

Premises used: DividedPowers.IsSubDPIdeal.self
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h : IsEmpty ι
⊢ hI.IsSubDPIdeal I

Tactic:
exact IsSubDPIdeal.self hI

Premises used: DividedPowers.IsSubDPIdeal.self
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ IsEmpty ι ∨ Nonempty ι

Tactic:
cases isEmpty_or_nonempty ι with
  | inr _ =>
    refine ⟨fun _ hx ↦ hx.1, ?_⟩
    intro n hn x hx
    simp only [Ideal.mem_inf, mem_iInf] at hx ⊢
    exact ⟨hI.dpow_mem hn hx.1, fun i ↦  IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩
  | inl _ =>
    simp only [iInf_of_empty, le_top, inf_of_le_left]
    exact IsSubDPIdeal.self hI

Premises used: iInf_of_empty, inf_of_le_left, isEmpty_or_nonempty, Ideal.mem_iInf, Ideal.mem_inf, le_top, DividedPowers.IsSubDPIdeal.self
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
rw :
  ∀ {n : ℕ},
    n ≠ 0 →
      ∀ (s : B),
        Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑K : Set A)) s →
          Membership.mem (γ := Ideal B) (span ((⇑f : (a : A) → B) '' (↑K : Set A))) (hJ.dpow n s)
rw₁ : (⇑f : (a : A) → B) '' (↑K : Set A) ⊆ (↑J : Set B)
⊢ hJ.IsSubDPIdeal (Ideal.map f K)

Tactic:
rw [Ideal.map, span_isSubDPIdeal_iff]

Premises used: Ideal.map, DividedPowers.span_isSubDPIdeal_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ (↑K : Set A)
⊢ Membership.mem (γ := Ideal B) (span ((⇑f : (a : A) → B) '' (↑K : Set A))) (hJ.dpow n ((f : (a : A) → B) x))

Tactic:
hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 _ hn hx)

Premises used: Ideal.mem_map_of_mem, Set.Mem, DividedPowers.IsSubDPIdeal.dpow_mem, Eq.rec, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.IsDPMorphism.dpow_comp, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ (↑K : Set A)
⊢ Membership.mem (γ := Ideal B) (span ((⇑f : (a : A) → B) '' (↑K : Set A))) (hJ.dpow n ((f : (a : A) → B) x))

Tactic:
exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 _ hn hx)
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
x : A
hx : x ∈ (↑K : Set A)
⊢ Membership.mem (α := B) (↑J : Set B) ((f : (a : A) → B) x : B)

Tactic:
hf.1 (mem_map_of_mem f (hK.1 hx))

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem, Set.Mem, DividedPowers.IsSubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
x : A
hx : x ∈ (↑K : Set A)
⊢ Membership.mem (α := B) (↑J : Set B) ((f : (a : A) → B) x : B)

Tactic:
exact hf.1 (mem_map_of_mem f (hK.1 hx))

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem, DividedPowers.IsSubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst_1 : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
⊢ hJ.IsSubDPIdeal (Ideal.map f I)

Tactic:
isSubDPIdeal_map_of_isSubDPIdeal hf (IsSubDPIdeal.self hI)

Premises used: DividedPowers.isSubDPIdeal_map_of_isSubDPIdeal, DividedPowers.IsSubDPIdeal.self
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h :
  Eq.{u_1 + 1} (α := Set A) ((fun (s : hI.SubDPIdeal) ↦ (↑s.carrier : Set A)) p)
    ((fun (s : hI.SubDPIdeal) ↦ (↑s.carrier : Set A)) q)
⊢ p.carrier = q.carrier

Tactic:
rw [SetLike.coe_set_eq] at h

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : p.carrier = q.carrier
mk :
  ∀ (carrier : Ideal A) (isSubideal : carrier ≤ I) (dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier)
    (h : { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal }.carrier = q.carrier),
    { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal } = q
⊢ p = q

Tactic:
cases p