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
refine_1 :
  ∀ (S : Set 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 }))
        (sSup S))
      (⨆ a ∈ S,
        (fun (J : hI.SubDPIdeal) ↦
            (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
          a)
refine_2 :
  ∀ (S : Set 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 }))
        (sInf S))
      (⨅ a ∈ S,
        (fun (J : hI.SubDPIdeal) ↦
            (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
          a)
⊢ CompleteLattice hI.SubDPIdeal

Tactic:
refine Function.Injective.completeLattice (fun J : SubDPIdeal hI ↦ (J : Set.Iic I))
    (fun J J' h ↦ by simpa only [SubDPIdeal.ext_iff, Subtype.mk.injEq] using h)
    .rfl .rfl (fun J J' ↦ by rfl) (fun J J' ↦ by rfl) (fun S ↦ ?_) (fun S ↦ ?_) rfl rfl

Premises used: DividedPowers.SubDPIdeal.isSubideal, Iff.rfl, DividedPowers.SubDPIdeal.carrier, Subtype.mk, Function.Injective.completeLattice, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
refine_1 :
  Eq.{u_1 + 1} (α := Ideal A)
    (↑((fun (J : hI.SubDPIdeal) ↦
            (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
          (sSup S)) :
      Ideal A)
    (sSup
      (Set.image (α := (↑(Set.Iic I) : Type u_1)) (val (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I))
        (Set.range fun (a : hI.SubDPIdeal) ↦
          ⨆ (_ : a ∈ S),
            (fun (J : hI.SubDPIdeal) ↦
                (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
              a)))
⊢ 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 }))
      (sSup S))
    (sSup
      (Set.range fun (a : hI.SubDPIdeal) ↦
        ⨆ (_ : a ∈ S),
          (fun (J : hI.SubDPIdeal) ↦
              (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
            a))

Tactic:
rw [Subtype.ext_iff, Set.Iic.coe_sSup]

Premises used: Subtype.ext_iff, Set.Iic.coe_sSup
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
refine_1 :
  Eq.{u_1 + 1} (α := Ideal A) (⨆ a ∈ S, (↑a : Ideal A))
    (⨆ (i : hI.SubDPIdeal),
      (↑(⨆ (_ : i ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) i.carrier ⋯) : Ideal A))
⊢ (sSup S).carrier =
    sSup
      (Set.image (α := (↑(Set.Iic I) : Type u_1)) (val (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I))
        (Set.range fun (a : hI.SubDPIdeal) ↦
          ⨆ (_ : a ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) a.carrier ⋯))

Tactic:
rw [sSup_carrier_def, sSup_image, sSup_image, iSup_range]

Premises used: iSup_range, DividedPowers.SubDPIdeal.sSup_carrier_def, sSup_image
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
pos :
  ∀ (hJ : J ∈ S),
    Eq.{u_1 + 1} (α := Ideal A)
      (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
      (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))
neg :
  ∀ (hJ : J ∉ S),
    Eq.{u_1 + 1} (α := Ideal A)
      (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
      (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))
⊢ Eq.{u_1 + 1} (α := Ideal A)
    (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
    (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))

Tactic:
by_cases hJ : J ∈ S
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ Eq.{u_1 + 1} (α := Ideal A)
    (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
    (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))

Tactic:
simp [ciSup_pos hJ]

Premises used: ciSup_pos
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ Eq.{u_1 + 1} (α := Ideal A)
    (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
    (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))

Tactic:
simp [hJ, not_false_eq_true, iSup_neg, Set.Iic.coe_bot]

Premises used: iSup_neg, not_false_eq_true, Set.Iic.coe_bot
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ∀ (J : hI.SubDPIdeal),
    Eq.{u_1 + 1} (α := Ideal A)
      (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
      (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))

Tactic:
have (J : hI.SubDPIdeal) :
      ((⨆ (_ : J ∈ S), (J : Set.Iic I) : Set.Iic I) : Ideal A) = ⨆ (_ : J ∈ S), (J : Ideal A) := by
      by_cases hJ : J ∈ S
      · simp [ciSup_pos hJ]
      · simp [hJ, not_false_eq_true, iSup_neg, Set.Iic.coe_bot]
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
this :
  ∀ (J : hI.SubDPIdeal),
    Eq.{u_1 + 1} (α := Ideal A)
      (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
      (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))
refine_1 : Eq.{u_1 + 1} (α := Ideal A) (⨆ a ∈ S, (↑a : Ideal A)) (⨆ i ∈ S, i.carrier)
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨆ a ∈ S, (↑a : Ideal A))
    (⨆ (i : hI.SubDPIdeal),
      (↑(⨆ (_ : i ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) i.carrier ⋯) : Ideal A))

Tactic:
simp_rw [this]
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
this :
  ∀ (J : hI.SubDPIdeal),
    Eq.{u_1 + 1} (α := Ideal A)
      (↑(⨆ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
      (⨆ (_ : J ∈ S), (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A))
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨆ a ∈ S, (↑a : Ideal A)) (⨆ i ∈ S, i.carrier)

Tactic:
rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
refine_2 :
  (↑((fun (J : hI.SubDPIdeal) ↦
            (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
          (sInf S)) :
      Ideal A) =
    I ⊓
      sInf
        (Set.image (α := (↑(Set.Iic I) : Type u_1)) (val (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I))
          (Set.range fun (a : hI.SubDPIdeal) ↦
            ⨅ (_ : a ∈ S),
              (fun (J : hI.SubDPIdeal) ↦
                  (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
                a))
⊢ 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 }))
      (sInf S))
    (sInf
      (Set.range fun (a : hI.SubDPIdeal) ↦
        ⨅ (_ : a ∈ S),
          (fun (J : hI.SubDPIdeal) ↦
              (Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯ : { x : Ideal A // x ∈ Set.Iic I }))
            a))

Tactic:
rw [Subtype.ext_iff, Set.Iic.coe_sInf]

Premises used: Set.Iic.coe_sInf, Subtype.ext_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
refine_2 :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (x : hI.SubDPIdeal), carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : x ∈ S), x.carrier)
    (⨅ (x : hI.SubDPIdeal),
      I ⊓ (↑(⨅ (_ : x ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) x.carrier ⋯) : Ideal A))
⊢ (sInf S).carrier =
    I ⊓
      sInf
        (Set.image (α := (↑(Set.Iic I) : Type u_1)) (val (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I))
          (Set.range fun (a : hI.SubDPIdeal) ↦
            ⨅ (_ : a ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) a.carrier ⋯))

Tactic:
rw [sInf_carrier_def, sInf_image, iInf_range, inf_iInf, iInf_insert, inf_iInf]

Premises used: DividedPowers.SubDPIdeal.sInf_carrier_def, iInf_range, sInf_image, inf_iInf, iInf_insert
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
apply :
  ∀ (J : hI.SubDPIdeal),
    carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
      I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨅ (x : hI.SubDPIdeal), carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : x ∈ S), x.carrier)
    (⨅ (x : hI.SubDPIdeal),
      I ⊓ (↑(⨅ (_ : x ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) x.carrier ⋯) : Ideal A))

Tactic:
apply iInf_congr (fun J ↦ ?_)

Premises used: iInf_congr
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
pos :
  ∀ (hJ : J ∈ S),
    carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
      I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
neg :
  ∀ (hJ : J ∉ S),
    carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
      I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
⊢ carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
    I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)

Tactic:
by_cases hJ : J ∈ S
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
pos :
  carrier (I := I) (hI := hI) ⊤ ⊓ J.carrier =
    I ⊓ (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)
⊢ carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
    I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)

Tactic:
rw [ciInf_pos hJ, ciInf_pos hJ]

Premises used: ciInf_pos
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ carrier (I := I) (hI := hI) ⊤ ⊓ J.carrier =
    I ⊓ (↑(Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
neg : carrier (I := I) (hI := hI) ⊤ = I
⊢ carrier (I := I) (hI := hI) ⊤ ⊓ ⨅ (_ : J ∈ S), J.carrier =
    I ⊓ (↑(⨅ (_ : J ∈ S), Subtype.mk (p := fun (x : Ideal A) ↦ x ∈ Set.Iic I) J.carrier ⋯) : Ideal A)

Tactic:
simp [hJ, iInf_neg, le_top, inf_of_le_left, Set.Iic.coe_top]

Premises used: inf_of_le_left, le_top, Set.Iic.coe_top, iInf_neg
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ carrier (I := I) (hI := hI) ⊤ = I

Tactic:
rfl
-- 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)
rw : {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ⊆ (↑I : Set A)
⊢ span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I

Tactic:
rw [span_le]

Premises used: Ideal.span_le
-- 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)
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ (↑I : Set A)

Tactic:
hxy ▸ hI.dpow_mem hn (hS hx)

Premises used: DividedPowers.dpow_mem, Eq.rec, 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)
y : A
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
hxy : y = hI.dpow n x
⊢ y ∈ (↑I : Set A)

Tactic:
exact hxy ▸ hI.dpow_mem hn (hS hx)
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
⊢ span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I

Tactic:
have hSI := hI.dpow_span_isSubideal hS
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
⊢ ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n z)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hz

Premises used: Submodule.span_induction
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
refine_1 :
  ∀ (x : A) (h : Membership.mem (γ := Set A) {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} x)
    (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n x)
refine_2 :
  ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n 0)
refine_3 :
  ∀ (x y : A)
    (hx :
      Membership.mem (γ := Submodule A A)
        (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) x)
    (hy :
      Membership.mem (γ := Submodule A A)
        (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) y),
    (∀ (n : ℕ),
        n ≠ 0 →
          Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
            (hI.dpow n x)) →
      (∀ (n : ℕ),
          n ≠ 0 →
            Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
              (hI.dpow n y)) →
        ∀ (n : ℕ),
          n ≠ 0 →
            Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
              (hI.dpow n (x + y))
refine_4 :
  ∀ (a x : A)
    (hx :
      Membership.mem (γ := Submodule A A)
        (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) x),
    (∀ (n : ℕ),
        n ≠ 0 →
          Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
            (hI.dpow n x)) →
      ∀ (n : ℕ),
        n ≠ 0 →
          Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
            (hI.dpow n (a • x))
⊢ ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n z)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hz
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
refine_1 :
  Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    ((↑(n.uniformBell m) : A) * hI.dpow (n * m) x)
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    (hI.dpow n y)

Tactic:
rw [hxy, hI.dpow_comp hm (hS hxS)]

Premises used: DividedPowers.dpow_comp
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    ((↑(n.uniformBell m) : A) * hI.dpow (n * m) x)

Tactic:
mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩)

Premises used: Ideal.subset_span, HMul.hMul, Exists.intro, mul_ne_zero, Ideal.mul_mem_left, rfl
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
y : A
m : ℕ
hm : m ≠ 0
x : A
hxS : x ∈ S
hxy : y = hI.dpow m x
n : ℕ
hn : n ≠ 0
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    ((↑(n.uniformBell m) : A) * hI.dpow (n * m) x)

Tactic:
exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩)
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
x : ℕ
hn : x ≠ 0
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    (hI.dpow x 0)

Tactic:
simp only [hI.dpow_eval_zero hn, zero_mem]

Premises used: DividedPowers.dpow_eval_zero, ZeroMemClass.zero_mem
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
⊢ ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n 0)

Tactic:
exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
-- 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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx :
  Membership.mem (γ := Submodule A A)
    (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) x
hy :
  Membership.mem (γ := Submodule A A)
    (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) y
hx_pow :
  ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n x)
hy_pow :
  ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n y)
n : ℕ
hn : n ≠ 0
refine_3 :
  Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    (∑ k ∈ Finset.range (n + 1), hI.dpow k x * hI.dpow (n - k) y)
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    (hI.dpow n (x + y))

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

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)
k : ℕ
hk : k ≠ 0
z : A
hz : Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) z
J : Ideal A := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx :
  Membership.mem (γ := Submodule A A)
    (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) x
hy :
  Membership.mem (γ := Submodule A A)
    (Submodule.span A {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}) y
hx_pow :
  ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n x)
hy_pow :
  ∀ (n : ℕ),
    n ≠ 0 →
      Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
        (hI.dpow n y)
n : ℕ
hn : n ≠ 0
refine_3 :
  ∀ c ∈ Finset.range (n + 1),
    Membership.mem (γ := Submodule A A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
      (hI.dpow c x * hI.dpow (n - c) y)
⊢ Membership.mem (γ := Ideal A) (span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x})
    (∑ k ∈ Finset.range (n + 1), hI.dpow k x * hI.dpow (n - k) y)

Tactic:
apply Submodule.sum_mem (span _)

Premises used: Submodule.sum_mem, Ideal.span