awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
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 : β),
      (((η : (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
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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∞)
⊢ ∫⁻ (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
have 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
Tactic: simp_rw [Set.preimage, Set.mem_setOf_eq, h_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: simp_rw [Set.preimage, Set.mem_setOf_eq, h_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
⊢ (κ ⊗ₖ η).fst = κ
have 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∞)
Tactic: ext x s hs
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (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
have 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
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)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (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
have 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
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)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (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
have 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
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)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (dividedPowers hI hJ).dpow n a = hI.dpow n a
have rw : (if a ∈ J then hI.dpow n a else 0) = hI.dpow n a
Tactic: rw [dpow_eq, if_pos ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ (dividedPowers hI hJ).dpow n a = hI.dpow n a
have rw₁ : hI.dpow n a = hI.dpow n a
Tactic: rw [dpow_eq, if_pos ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ hI.dpow x x_1 = (dividedPowers hI hJ).dpow x x_1
have rw : hI.dpow x x_1 = hI.dpow x x_1
Tactic: rw [dpow_eq_of_mem _ _ ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
have 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
Tactic: refine ⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
have 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)
Tactic: refine ⟨fun hIJ n a b ha hb hab ↦ ?_, fun hIJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (hypothesis)
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
⊢ hI.dpow n a - hI.dpow n b ∈ J
have hab' : a - b ∈ I
Tactic: have hab' : a - b ∈ I := I.sub_mem ha hb
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ hI.dpow n a - hI.dpow n b ∈ J
have refine_1 : ∑ x ∈ range n, hI.dpow x b * hI.dpow (n - x) (a - 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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
have refine_2 : ∀ {n : ℕ} (hn : n ≠ 0) {a : A} (ha : a ∈ J ⊓ I), hI.dpow n a ∈ (↑J : Set A)
Tactic: refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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 ∈ (↑J : Set A)
have refine_2 : hI.dpow n a - hI.dpow n 0 ∈ (↑J : Set A)
Tactic: rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
have refine : ∀ (hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, Membership.mem (γ := Ideal A) (span S) (hI.dpow n s)), hI.IsSubDPIdeal (span S)
Tactic: refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem n hn (subset_span hs), fun hhI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (hypothesis)
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)
⊢ hI.IsSubDPIdeal (span S)
have hSI : span S ≤ I
Tactic: have hSI := span_le.mpr hS
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ hI.IsSubDPIdeal (span S)
have apply : ∀ (n : ℕ),
  n ≠ 0 → ∀ {j : A}, Membership.mem (γ := Ideal A) (span S) j → Membership.mem (γ := Ideal A) (span S) (hI.dpow n j)
Tactic: apply IsSubDPIdeal.mk hSI
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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) (hI.dpow m 0)
have zero : Membership.mem (γ := Ideal A) (span S) 0
Tactic: rw [hI.dpow_eval_zero hm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m (x + y))
have add : Membership.mem (γ := Ideal A) (span S) (∑ k ∈ range (m + 1), hI.dpow k x * hI.dpow (m - k) y)
Tactic: rw [hI.dpow_add' (hSI hxI) (hSI hyI)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ Membership.mem (γ := Ideal A) (span S) (∑ k ∈ range (m + 1), hI.dpow k x * hI.dpow (m - k) y)
have add : ∀ c ∈ range (m + 1), Membership.mem (γ := Submodule A A) (span S) (hI.dpow c x * hI.dpow (m - c) y)
Tactic: apply Submodule.sum_mem (span S)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
have pos : ∀ (hm0 : m = 0), Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
have neg : ∀ (hm0 : ¬m = 0), Membership.mem (γ := Submodule A A) (span S) (hI.dpow m x * hI.dpow (m_1 - m) y)
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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) (hI.dpow m (a • x))
have smul : Membership.mem (γ := Ideal A) (span S) (a ^ m * hI.dpow m x)
Tactic: rw [smul_eq_mul, hI.dpow_mul (hSI hxI)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m z)
have mem : ∀ (x : A) (h : x ∈ S) (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m x)
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)
Cleared hypotheses: m, hm, hz
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m z)
have zero : ∀ (m : ℕ) (hm : m ≠ 0), Membership.mem (γ := Ideal A) (span S) (hI.dpow m 0)
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)
Cleared hypotheses: m, hm, hz
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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)
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m z)
have 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))
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)
Cleared hypotheses: m, hm, hz
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
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))
⊢ Membership.mem (γ := Ideal A) (span S) (hI.dpow m z)
have 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))
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)
Cleared hypotheses: m, hm, hz