awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : ¬Multipliable f L
⊢ ¬Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L
have neg : ∀ (h : Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L), Multipliable f L
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L
⊢ Multipliable f L
have h₁ : ∃ (a : α'), Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 a)
Tactic: simp only [Multipliable, HasProd] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : ∃ (a : α'), Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 a)
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
have neg : ∀ (b : α') (hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)),
  ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
have neg : ∀ (a : α) (ha : (g : (a : α) → α') a = b), ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Tactic: obtain ⟨a, ha⟩ : b ∈ Set.range g :=
        hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod])
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
a : α
ha : (g : (a : α) → α') a = b
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
have h : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
⊢ Multipliable f L ↔
    Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have mp : Multipliable f L →
  Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
mp :
  Multipliable f L →
    Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Multipliable f L ↔
    Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have mpr : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i)) →
  Multipliable f L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have mp : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
mp : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have mp₁ : Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
  (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have pos : ∀ (hL : L.NeBot),
  Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
pos :
  ∀ (hL : L.NeBot),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have neg : ∀ (hL : ¬L.NeBot),
  Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have pos : ∀ (hfs : Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))),
  Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
pos :
  ∀ (hfs : Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
have neg : ∀ (hfs : ¬Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))),
  Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
Tactic: by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
⊢ Multipliable f L
have h : HasProd f a L
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
⊢ HasProd f a L
have this : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) (∏'[L] (b : β), ((⇑g : (a : α) → γ) ∘ f) b) L
Tactic: have := hgf.hasProd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
this : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) (∏'[L] (b : β), ((⇑g : (a : α) → γ) ∘ f) b) L
⊢ HasProd f a L
have this₁ : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L
Tactic: simp_rw [comp_apply, ← ha] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))
have simp_rw : Tendsto (fun (s : Finset β) ↦ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏ x ∈ s, g x)) L.filter (𝓝 (a * b))
Tactic: simp_rw [prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : HasProd f a L
n : ℕ
⊢ HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L
have zero : HasProd (fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0) (HPow.hPow (β := ℕ) a 0) L
Tactic: induction n with
  | zero => simp
  | succ n hn => simpa [pow_succ] using hn.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : HasProd f a L
n : ℕ
zero : HasProd (fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0) (HPow.hPow (β := ℕ) a 0) L
⊢ HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L
have succ : ∀ (n : ℕ) (hn : HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L), HasProd (fun (x : β) ↦ f x ^ (n + 1)) (a ^ (n + 1)) L
Tactic: induction n with
  | zero => simp
  | succ n hn => simpa [pow_succ] using hn.mul hf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        (∀ i ∈ insert a_1 s, HasProd (f i) (a i) L) →
          HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ insert a_1 s, f i b) (∏ i ∈ insert a_1 s, a i) L
have simp : ∀ (a_1 : γ) (s : Finset γ),
  a_1 ∉ s →
    ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
      HasProd (f a_1) (a a_1) L →
        (∀ a_5 ∈ s, HasProd (f a_5) (a a_5) L) →
          HasProd (fun (b : β) ↦ f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i) L
Tactic: simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a
hb : HasProd (β := (↑t : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t)) b
⊢ HasProd (β := (↑(s ∪ t) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s ∪ t)) (a * b)
have rw : ∀ (ha : HasProd (s.mulIndicator f) a) (hb : HasProd (t.mulIndicator f) b), HasProd ((s ∪ t).mulIndicator f) (a * b)
Tactic: rw [hasProd_subtype_iff_mulIndicator] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)
have rw : HasProd (fun (a : β) ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)
Tactic: rw [Set.mulIndicator_union_of_disjoint hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (β := (↑(t i) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t i)) (a i)
⊢ HasProd (β := (↑(⋃ i ∈ s, t i) : Type u_2))
    (f ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) (⋃ i ∈ s, t i) x)) (∏ i ∈ s, a i)
have simp_rw : ∀ (hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)), HasProd (Set.mulIndicator (⋃ i ∈ s, t i) f) (∏ i ∈ s, a i)
Tactic: simp_rw [hasProd_subtype_iff_mulIndicator] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd (Set.mulIndicator (⋃ i ∈ s, t i) f) (∏ i ∈ s, a i)
have rw : HasProd.{u_1, u_2} (α := α) (fun (a : β) ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)
Tactic: rw [Finset.mulIndicator_biUnion _ _ hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
b' : β
⊢ (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
have pos : ∀ (hb' : b' = b), f b' * x = update (β := fun (a : β) ↦ α) f b x b' * f b
Tactic: split_ifs with hb'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
b' : β
pos : ∀ (hb' : b' = b), f b' * x = update (β := fun (a : β) ↦ α) f b x b' * f b
⊢ (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
have neg : ∀ (hb' : ¬b' = b), f b' * 1 = update (β := fun (a : β) ↦ α) f b x b' * 1
Tactic: split_ifs with hb'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
⊢ a * x = a' * f b
have this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
Tactic: have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 := by
    intro b'
    split_ifs with hb'
    · simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x
    · simp only [Function.update_apply, hb', if_false]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
⊢ a * x = a' * f b
have h : HasProd (fun (b_1 : β) ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
Tactic: have h := hf.mul (hasProd_ite_eq b x L)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
h : HasProd (fun (b_1 : β) ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ a * x = a' * f b
have h₁ : HasProd (fun (b_1 : β) ↦ update (β := fun (a : β) ↦ α) f b x b_1 * if b_1 = b then f b else 1) (a * x) L
Tactic: simp_rw [this] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
⊢ a = a' * f b
have refine : HasProd (update (β := fun (a : β) ↦ α) f b 1) a' L
Tactic: refine (mul_one a).symm.trans (hf.update' b 1 ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
⊢ HasProd (update (β := fun (a : β) ↦ α) f b 1) a' L
have h : ∀ (x : β), update (β := fun (a : β) ↦ α) f b 1 x = if x = b then 1 else f x
Tactic: convert! hf'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s t : Set β
h : s = t
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : (↑t : Type u_2)), f (↑x : β))
have rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑t : Type u_2)), f (↑x : β)) (∏' (x : (↑t : Type u_2)), f (↑x : β))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
s : Finset β
hf : mulSupport f ⊆ (↑s : Set β)
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b ∈ s, f b)
have rw : Eq.{u_1 + 1} (α := α) (∏ᶠ (b : β), f b) (∏ b ∈ s, f b)
Tactic: rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf]