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
q : hI.SubDPIdeal
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
mk :
  ∀ (carrier_1 : Ideal A) (isSubideal_1 : carrier_1 ≤ I)
    (dpow_mem_1 : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier_1, hI.dpow n j ∈ carrier_1)
    (h :
      { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal }.carrier =
        { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 : hI.SubDPIdeal }.carrier),
    { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal } =
      { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 }
⊢ { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal } = q

Tactic:
cases q
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
carrier : Ideal A
isSubideal : carrier ≤ I
dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier
carrier_1 : Ideal A
isSubideal_1 : carrier_1 ≤ I
dpow_mem_1 : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier_1, hI.dpow n j ∈ carrier_1
h :
  { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal }.carrier =
    { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 : hI.SubDPIdeal }.carrier
⊢ { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem : hI.SubDPIdeal } =
    { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : hI.SubDPIdeal
⊢ (↑J : Ideal A) = J.carrier

Tactic:
rfl

Premises used: DividedPowers.SubDPIdeal.toIdeal, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
s : hI.SubDPIdeal
x : A
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
smul : b ^ m * hI.dpow m a ∈ J * I
⊢ hI.dpow m (a • b) ∈ I • J

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_mul ha, mul_comm]

Premises used: DividedPowers.dpow_mul, mul_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ b ^ m * hI.dpow m a ∈ J * I

Tactic:
Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm))
        (hI.dpow_mem hm ha)

Premises used: DividedPowers.dpow_mem, Iff.mpr, Submodule.mul_mem_mul, Set.Mem, Ideal.pow_mem_of_mem, zero_lt_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ b ^ m * hI.dpow m a ∈ J * I

Tactic:
exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm))
        (hI.dpow_mem hm ha)

Premises used: DividedPowers.dpow_mem, Iff.mpr, Submodule.mul_mem_mul, Ideal.pow_mem_of_mem, zero_lt_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
add : ∑ k ∈ Finset.range (m + 1), hI.dpow k x * hI.dpow (m - k) y ∈ I • J
⊢ hI.dpow m (x + y) ∈ I • J

Tactic:
rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)]

Premises used: Ideal.mul_le_right, DividedPowers.dpow_add'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
add : ∀ c ∈ Finset.range (m + 1), hI.dpow c x * hI.dpow (m - c) y ∈ I • J
⊢ ∑ k ∈ Finset.range (m + 1), hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
apply Submodule.sum_mem (I • J)

Premises used: Submodule.sum_mem, HSMul.hSMul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
add : k ∈ Finset.range (m + 1) → hI.dpow k x * hI.dpow (m - k) y ∈ I • J
⊢ k ∈ Finset.range (m + 1) → hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
_
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
h : k ∈ Finset.range (m + 1)
pos : ∀ (hk0 : k = 0), hI.dpow k x * hI.dpow (m - k) y ∈ I • J
neg : ∀ (hk0 : ¬k = 0), hI.dpow k x * hI.dpow (m - k) y ∈ I • J
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
by_cases hk0 : k = 0
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
h : k ∈ Finset.range (m + 1)
hk0 : k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)

Premises used: Eq.rec, HSMul.hSMul, 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
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
h : k ∈ Finset.range (m + 1)
hk0 : k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
h : k ∈ Finset.range (m + 1)
hk0 : ¬k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
mul_mem_right _ (I • J) (hx' k hk0)

Premises used: Set.Mem, Ideal.mul_mem_right, HSMul.hSMul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x_1 x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
h : k ∈ Finset.range (m + 1)
hk0 : ¬k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
exact mul_mem_right _ (I • J) (hx' k hk0)

Premises used: Ideal.mul_mem_right, HSMul.hSMul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I • J
smul : ∀ (a : A) (ha : a ∈ I) (b : A) (hb : b ∈ J) (m : ℕ) (hm : m ≠ 0), hI.dpow m (a • b) ∈ I • J
add :
  ∀ (x : A) (hx : x ∈ I • J) (y : A) (hy : y ∈ I • J) (hx' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m x ∈ I • J)
    (hy' : ∀ (m : ℕ) (hm : m ≠ 0), hI.dpow m y ∈ I • J) (m : ℕ) (hm : m ≠ 0), hI.dpow m (x + y) ∈ I • J
⊢ hI.dpow m x ∈ I • J

Tactic:
induction hx using Submodule.smul_induction_on' generalizing m with
    | smul a ha b hb =>
      rw [smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_mul ha, mul_comm]
      exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm))
        (hI.dpow_mem hm ha)
    | add x hx y hy hx' hy' =>
      rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)]
      apply Submodule.sum_mem (I • J)
      intro k _
      by_cases hk0 : k = 0
      · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)
      · exact mul_mem_right _ (I • J) (hx' k hk0)

Premises used: Submodule.sum_mem, mul_comm, HSMul.hSMul, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ J ≤ J' ↔ J.carrier ≤ J'.carrier

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ J < J' ↔ J.carrier < J'.carrier

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
rw : Membership.mem (γ := Ideal A) ⊥ (hI.dpow x_1 0)
rw₁ : Membership.mem (γ := Ideal A) ⊥ 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 0 0
⊢ Membership.mem (γ := Ideal A) ⊥ (hI.dpow x_1 x)

Tactic:
rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]

Premises used: Ideal.mem_bot, DividedPowers.dpow_eval_zero, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ (J ⊓ J').carrier = J.carrier ⊓ J'.carrier

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x : A
hx : Membership.mem (γ := Submodule A A) (⨅ s ∈ insert ⊤ S, s.carrier) x
⊢ ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier

Tactic:
simp only [mem_iInf] at hx

Premises used: Ideal.mem_iInf
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x : A
hx : ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier
⊢ x ∈ I

Tactic:
hx ⊤ (Set.mem_insert ⊤ S)

Premises used: Set.Mem, Set.mem_insert, Top.top
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x : A
hx : ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier
⊢ x ∈ I

Tactic:
exact hx ⊤ (Set.mem_insert ⊤ S)

Premises used: Set.mem_insert, Top.top
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : Membership.mem (γ := Ideal A) (⨅ s ∈ insert ⊤ S, s.carrier) x
simp :
  ∀ (hx : ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier) (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S),
    hI.dpow x_1 x ∈ i.carrier
⊢ Membership.mem (γ := Ideal A) (⨅ s ∈ insert ⊤ S, s.carrier) (hI.dpow x_1 x)

Tactic:
simp only [mem_iInf] at hx ⊢

Premises used: Ideal.mem_iInf
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier
⊢ ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), hI.dpow x_1 x ∈ i.carrier

Tactic:
fun s hs ↦ s.dpow_mem _ hn x (hx s hs)

Premises used: DividedPowers.SubDPIdeal.dpow_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), x ∈ i.carrier
⊢ ∀ (i : hI.SubDPIdeal) (i_1 : i ∈ insert ⊤ S), hI.dpow x_1 x ∈ i.carrier

Tactic:
exact fun s hs ↦ s.dpow_mem _ hn x (hx s hs)
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ (sInf S).carrier = ⨅ s ∈ insert ⊤ S, s.carrier

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ (J ⊔ J').carrier = (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) (J ⊔ J').carrier ⋯) : Ideal A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ :
  Membership.mem (γ := Set A)
    ((fun (i : Ideal A) ↦
        (⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) :
          Set A))
      J)
    a
⊢ Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J ∧ a ∈ J

Tactic:
rw [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at haJ

Premises used: Set.mem_iUnion, exists_prop, SetLike.mem_coe
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J ∧ a ∈ J
obtain : ∀ (J' : hI.SubDPIdeal) (hJ' : J' ∈ S ∧ J'.carrier = J), a ∈ (↑I : Set A)
⊢ a ∈ (↑I : Set A)

Tactic:
obtain ⟨J', hJ'⟩ := (Set.mem_image _ _ _).mp haJ.1

Premises used: Set.mem_image, And.left, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J ∧ a ∈ J
J' : hI.SubDPIdeal
hJ' : J' ∈ S ∧ J'.carrier = J
⊢ a ∈ (↑I : Set A)

Tactic:
J'.isSubideal  (hJ'.2 ▸ haJ.2)

Premises used: Set.Mem, DividedPowers.SubDPIdeal.isSubideal, Eq.rec, And.right, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
a : A
J : Ideal A
haJ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J ∧ a ∈ J
J' : hI.SubDPIdeal
hJ' : J' ∈ S ∧ J'.carrier = J
⊢ a ∈ (↑I : Set A)

Tactic:
exact  J'.isSubideal  (hJ'.2 ▸ haJ.2)

Premises used: DividedPowers.SubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)

Tactic:
have h : (⋃ (i : Ideal A) (_ : i ∈ (fun J ↦ J.carrier) '' S), ↑i) ⊆ (I : Set A) := by
        rintro a ⟨-, ⟨J, rfl⟩, haJ⟩
        rw [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at haJ
        obtain ⟨J', hJ'⟩ := (Set.mem_image _ _ _).mp haJ.1
        exact  J'.isSubideal  (hJ'.2 ▸ haJ.2)
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
rw :
  ∀ {n : ℕ},
    n ≠ 0 →
      ∀ (s : A),
        Membership.mem (γ := Set A)
            (⋃ (i : Ideal A),
              ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A))
            s →
          Membership.mem (γ := Ideal A)
            (span
              (⋃ (i : Ideal A),
                ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i),
                  (↑i : Set A)))
            (hI.dpow n s)
⊢ hI.IsSubDPIdeal (sSup ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S))

Tactic:
rw [sSup_eq_iSup, Submodule.iSup_eq_span', submodule_span_eq, span_isSubDPIdeal_iff h]

Premises used: Ideal.submodule_span_eq, sSup_eq_iSup, DividedPowers.span_isSubDPIdeal_iff, Submodule.iSup_eq_span'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
n : ℕ
hn : n ≠ 0
x : A
J : Ideal A
hJ' : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J
h' :
  Membership.mem (γ := Set A)
    ((fun (x : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J) ↦ (↑J : Set A)) hJ')
    x
a :
  Membership.mem (γ := Set A)
    (⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A))
    (hI.dpow n x)
⊢ Membership.mem (γ := Ideal A)
    (span
      (⋃ (i : Ideal A),
        ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A)))
    (hI.dpow n x)

Tactic:
apply subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
n : ℕ
hn : n ≠ 0
x : A
J : Ideal A
hJ' : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J
h' :
  Membership.mem (γ := Set A)
    ((fun (x : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J) ↦ (↑J : Set A)) hJ')
    x
a : hI.dpow n x ∈ (↑J : Set A)
⊢ Membership.mem (γ := Set A)
    (⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A))
    (hI.dpow n x)

Tactic:
apply Set.mem_biUnion hJ'

Premises used: Set.mem_biUnion
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
n : ℕ
hn : n ≠ 0
x : A
J : Ideal A
hJ' : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J
h' :
  Membership.mem (γ := Set A)
    ((fun (x : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) J) ↦ (↑J : Set A)) hJ')
    x
a :
  ∀ (K : hI.SubDPIdeal) (hKS : K ∈ S)
    (h' :
      Membership.mem (γ := Set A)
        ((fun
              (x :
                Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S)
                  ((fun (J : hI.SubDPIdeal) ↦ J.carrier) K)) ↦
            (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A))
          ⋯)
        x),
    hI.dpow n x ∈ (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A)
⊢ hI.dpow n x ∈ (↑J : Set A)

Tactic:
obtain ⟨K, hKS, rfl⟩ := hJ'

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
n : ℕ
hn : n ≠ 0
x : A
K : hI.SubDPIdeal
hKS : K ∈ S
h' :
  Membership.mem (γ := Set A)
    ((fun
          (x :
            Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S)
              ((fun (J : hI.SubDPIdeal) ↦ J.carrier) K)) ↦
        (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A))
      ⋯)
    x
⊢ hI.dpow n x ∈ (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A)

Tactic:
K.dpow_mem _ hn x h'

Premises used: Set.Mem, DividedPowers.SubDPIdeal.dpow_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h :
  ⋃ (i : Ideal A),
      ⋃ (_ : Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S) i), (↑i : Set A) ⊆
    (↑I : Set A)
n : ℕ
hn : n ≠ 0
x : A
K : hI.SubDPIdeal
hKS : K ∈ S
h' :
  Membership.mem (γ := Set A)
    ((fun
          (x :
            Membership.mem (γ := Set (Ideal A)) ((fun (J : hI.SubDPIdeal) ↦ J.carrier) '' S)
              ((fun (J : hI.SubDPIdeal) ↦ J.carrier) K)) ↦
        (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A))
      ⋯)
    x
⊢ hI.dpow n x ∈ (↑((fun (J : hI.SubDPIdeal) ↦ J.carrier) K) : Set A)

Tactic:
exact K.dpow_mem _ hn x h'

Premises used: DividedPowers.SubDPIdeal.dpow_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ (sSup S).carrier = sSup (toIdeal '' S)

Tactic:
rfl

Premises used: DividedPowers.SubDPIdeal.toIdeal, Set.Mem, setOf, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
h :
  Eq.{u_1 + 1} (α := { x : Ideal A // x ∈ Set.Iic I })
    ((fun (J : hI.SubDPIdeal) ↦
        (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
      J)
    ((fun (J : hI.SubDPIdeal) ↦
        (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
      J')
⊢ J = J'

Tactic:
simpa only [SubDPIdeal.ext_iff, Subtype.mk.injEq] using h

Premises used: DividedPowers.SubDPIdeal.ext_iff, Subtype.mk.injEq
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ Eq.{u_1 + 1} (α := { x : Ideal A // x ∈ Set.Iic I })
    ((fun (J : hI.SubDPIdeal) ↦
        (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
      (J ⊔ J'))
    ((fun (J : hI.SubDPIdeal) ↦
          (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
        J ⊔
      (fun (J : hI.SubDPIdeal) ↦
          (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
        J')

Tactic:
rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ Eq.{u_1 + 1} (α := { x : Ideal A // x ∈ Set.Iic I })
    ((fun (J : hI.SubDPIdeal) ↦
        (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
      (J ⊓ J'))
    ((fun (J : hI.SubDPIdeal) ↦
          (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
        J ⊓
      (fun (J : hI.SubDPIdeal) ↦
          (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
        J')

Tactic:
rfl