awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ MeasurableSet (Prod.map id f '' t)

Tactic:
exact (MeasurableEmbedding.id.prodMap hf).measurableSet_image.mpr ht

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasurableEmbedding.prodMap, MeasurableEmbedding.id
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' {p : β × γ | p.1 ∈ s}) ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
hs₁ : MeasurableSet (α := β × γ) {p : β × γ | p.1 ∈ s}
⊢ ((((κ ⊗ₖ η).fst : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x

Tactic:
rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]

Premises used: ProbabilityTheory.Kernel.fst_apply', ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := β × γ) {p : β × γ | p.1 ∈ s}

Tactic:
measurable_fst hs

Premises used: Set.preimage, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := β × γ) {p : β × γ | p.1 ∈ s}

Tactic:
exact measurable_fst hs

Premises used: measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
b : β
pos :
  ∀ (hb : b ∈ s),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
          b :
        ℝ≥0∞)
neg :
  ∀ (hb : b ∉ s),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
          b :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ) b :
      ℝ≥0∞)

Tactic:
by_cases hb : b ∈ s
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
b : β
hb : b ∈ s
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ) b :
      ℝ≥0∞)

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
b : β
hb : b ∉ s
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ) b :
      ℝ≥0∞)

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
          b :
        ℝ≥0∞)

Tactic:
have h_eq b : η (x, b) {c | b ∈ s} = s.indicator (fun b ↦ η (x, b) Set.univ) b := by
    by_cases hb : b ∈ s <;> simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
h_eq :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
          b :
        ℝ≥0∞)
simp_rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | Membership.mem (γ := Set (β × γ)) {p : β × γ | p.1 ∈ s} (b, x)} ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
simp_rw₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' {p : β × γ | p.1 ∈ s}) ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x

Tactic:
simp_rw [Set.preimage, Set.mem_setOf_eq, h_eq]

Premises used: Set.mem_setOf_eq, Set.preimage
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
h :
  ∀ (x : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((((κ ⊗ₖ η).fst : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ ⊗ₖ η).fst = κ

Tactic:
ext x s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ ⊗ₖ η).fst : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [fst_compProd_apply, hs]

Premises used: ProbabilityTheory.Kernel.fst_compProd_apply
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
x : A
hx : x ∉ J
⊢ (if x ∈ J then hI.dpow n x else 0) = 0

Tactic:
simp [if_neg hx]

Premises used: if_neg
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
x : A
hx : x ∈ J
⊢ (if x ∈ J then hI.dpow 0 x else 0) = 1

Tactic:
simp [if_pos hx, hI.dpow_zero (hJ.isSubideal hx)]

Premises used: if_pos, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.dpow_zero
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
x : A
hx : x ∈ J
⊢ (if x ∈ J then hI.dpow 1 x else 0) = x

Tactic:
simp [if_pos hx, hI.dpow_one (hJ.isSubideal hx)]

Premises used: if_pos, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.dpow_one
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ J
⊢ (if x ∈ J then hI.dpow n x else 0) ∈ J

Tactic:
simp [if_pos hx, hJ.dpow_mem _ hn hx]

Premises used: DividedPowers.IsSubDPIdeal.dpow_mem, if_pos
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
x y : A
hx : x ∈ J
hy : y ∈ J
simp_rw :
  (if x + y ∈ J then hI.dpow n (x + y) else 0) =
    ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, hI.dpow x_1.1 x * if y ∈ J then hI.dpow x_1.2 y else 0
simp_rw₁ :
  (if x + y ∈ J then hI.dpow n (x + y) else 0) =
    ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, hI.dpow x_1.1 x * hI.dpow x_1.2 y
simp_rw₂ : hI.dpow n (x + y) = ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, hI.dpow x_1.1 x * hI.dpow x_1.2 y
⊢ (if x + y ∈ J then hI.dpow n (x + y) else 0) =
    ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      (if x ∈ J then hI.dpow k.1 x else 0) * if y ∈ J then hI.dpow k.2 y else 0

Tactic:
simp_rw [if_pos hx, if_pos hy, if_pos (Ideal.add_mem J hx hy),
    hI.dpow_add (hJ.isSubideal hx) (hJ.isSubideal hy)]

Premises used: DividedPowers.dpow_add, Ideal.add_mem, if_pos, DividedPowers.IsSubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
a x : A
hx : x ∈ J
⊢ (if a * x ∈ J then hI.dpow n (a * x) else 0) = a ^ n * if x ∈ J then hI.dpow n x else 0

Tactic:
simp [if_pos hx, if_pos (mul_mem_left J _ hx), hI.dpow_mul (hJ.isSubideal hx)]

Premises used: if_pos, DividedPowers.IsSubDPIdeal.isSubideal, DividedPowers.dpow_mul, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
m n : ℕ
x : A
hx : x ∈ J
⊢ ((if x ∈ J then hI.dpow m x else 0) * if x ∈ J then hI.dpow n x else 0) =
    (↑((m + n).choose m) : A) * if x ∈ J then hI.dpow (m + n) x else 0

Tactic:
simp [if_pos hx, hI.mul_dpow (hJ.isSubideal hx)]

Premises used: if_pos, DividedPowers.mul_dpow, DividedPowers.IsSubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
m n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ J
⊢ (if (if x ∈ J then hI.dpow n x else 0) ∈ J then hI.dpow m (if x ∈ J then hI.dpow n x else 0) else 0) =
    (↑(m.uniformBell n) : A) * if x ∈ J then hI.dpow (m * n) x else 0

Tactic:
simp [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]

Premises used: DividedPowers.dpow_comp, DividedPowers.IsSubDPIdeal.dpow_mem, if_pos, DividedPowers.IsSubDPIdeal.isSubideal
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
a : A
⊢ (dividedPowers hI hJ).dpow n a = if a ∈ J then hI.dpow n a else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst_1 : (x : A) → Decidable (x ∈ J)
n : ℕ
a : A
ha : a ∈ J
rw : (if a ∈ J then hI.dpow n a else 0) = hI.dpow n a
rw₁ rw₂ : hI.dpow n a = hI.dpow n a
⊢ (dividedPowers hI hJ).dpow n a = hI.dpow n a

Tactic:
rw [dpow_eq, if_pos ha]

Premises used: if_pos, DividedPowers.IsSubDPIdeal.dpow_eq
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst_1 : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
x : ℕ
h : x ≠ 0
x_1 : A
ha : x_1 ∈ J
rw rw₁ : hI.dpow x x_1 = hI.dpow x x_1
⊢ hI.dpow x x_1 = (dividedPowers hI hJ).dpow x x_1

Tactic:
rw [dpow_eq_of_mem _ _ ha]

Premises used: DividedPowers.IsSubDPIdeal.dpow_eq_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst_1 : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
⊢ (dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)

Tactic:
simpa only [isDPMorphism_iff, Ideal.map_id, RingHom.id_apply]
    using ⟨hJ.1, fun _ _ _ ha ↦ by rw [dpow_eq_of_mem _ _ ha]⟩

Premises used: RingHom.id_apply, Ideal.map_id, DividedPowers.isDPMorphism_iff
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J

Tactic:
⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
refine_1 :
  ∀ (hIJ : hI.IsSubDPIdeal (J ⊓ I)) (n : ℕ) (a b : A) (ha : a ∈ I) (hb : b ∈ I) (hab : a - b ∈ J),
    hI.dpow n a - hI.dpow n b ∈ J
refine_2 :
  ∀ (hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J), hI.IsSubDPIdeal (J ⊓ I)
⊢ hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J

Tactic:
refine ⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ a - b ∈ I

Tactic:
have hab' : a - b ∈ I := I.sub_mem ha hb
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
refine_1 : ∑ x ∈ range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J

Tactic:
rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_add_one, sum_insert notMem_range_self,
      tsub_self, hI.dpow_zero hab', mul_one, add_sub_cancel_left]

Premises used: add_sub_cancel_left, tsub_self, Finset.range_add_one, DividedPowers.dpow_zero, add_sub_cancel, Finset.notMem_range_self, DividedPowers.dpow_add', mul_one, Finset.sum_insert
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J

Tactic:
J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
      (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))

Premises used: Set.Mem, Nat.sub_pos_of_lt, Submodule.sum_mem, HSub.hSub, SemilatticeInf.inf_le_left, DividedPowers.IsSubDPIdeal.dpow_mem, ne_of_gt, Finset.mem_range, DividedPowers.dpow, And.intro, Iff.mp, Min.min, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J

Tactic:
exact J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
      (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))

Premises used: Nat.sub_pos_of_lt, Submodule.sum_mem, HSub.hSub, SemilatticeInf.inf_le_left, DividedPowers.IsSubDPIdeal.dpow_mem, ne_of_gt, Finset.mem_range, And.intro, Iff.mp, Min.min, Submodule.smul_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.IsSubDPIdeal (J ⊓ I)

Tactic:
⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩

Premises used: DividedPowers.dpow_mem, SemilatticeInf.inf_le_right, And.right, And.intro, DividedPowers.IsSubDPIdeal.mk
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
refine_2 : ∀ {n : ℕ} (hn : n ≠ 0) {a : A} (ha : a ∈ J ⊓ I), hI.dpow n a ∈ (↑J : Set A)
⊢ hI.IsSubDPIdeal (J ⊓ I)

Tactic:
refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
refine_2 : hI.dpow n a - hI.dpow n 0 ∈ (↑J : Set A)
⊢ hI.dpow n a ∈ (↑J : Set A)

Tactic:
rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]

Premises used: sub_zero, DividedPowers.dpow_eval_zero, DividedPowers.dpow
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ (↑J : Set A)

Tactic:
hIJ ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)

Premises used: Set.Mem, Ideal.zero_mem, And.right, And.left, Ideal.sub_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ (↑J : Set A)

Tactic:
exact hIJ ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)

Premises used: Ideal.zero_mem, And.right, And.left, Ideal.sub_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)
⊢ hI.IsSubDPIdeal (span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)

Tactic:
⟨fun hhI n hn s hs ↦ hhI.dpow_mem n hn (subset_span hs), fun hhI ↦ ?_⟩

Premises used: Ideal.subset_span, DividedPowers.IsSubDPIdeal.dpow_mem, Iff.intro
-- 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)
refine :
  ∀ (hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)), hI.IsSubDPIdeal (span S)
⊢ hI.IsSubDPIdeal (span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)

Tactic:
refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem n hn (subset_span hs), fun hhI ↦ ?_⟩
-- 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)
⊢ span S ≤ I

Tactic:
have hSI := span_le.mpr 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)
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)
hSI : span S ≤ I
apply :
  ∀ (n : ℕ),
    n ≠ 0 → ∀ {j : A}, Membership.mem (γ := Ideal A) (span S) j → Membership.mem (γ := Ideal A) (span S) (hI.dpow n j)
⊢ hI.IsSubDPIdeal (span S)

Tactic:
apply IsSubDPIdeal.mk hSI

Premises used: DividedPowers.IsSubDPIdeal.mk
-- 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 : A
h : x ∈ S
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)

Tactic:
hhI hm x h
-- 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 : A
h : x ∈ S
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)

Tactic:
exact hhI hm x h
-- 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
m : ℕ
hm : m ≠ 0
zero : Membership.mem (γ := Ideal A) (span S) 0
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m 0)

Tactic:
rw [hI.dpow_eval_zero hm]

Premises used: DividedPowers.dpow_eval_zero
-- 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
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) 0

Tactic:
(span S).zero_mem

Premises used: Ideal.zero_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 : A
m : ℕ
hm : m ≠ 0
⊢ Membership.mem (γ := Ideal A) (span S) 0

Tactic:
exact (span S).zero_mem

Premises used: Ideal.zero_mem, Ideal.span