awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ HasProd g (c * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i))
have refine : EventuallyEq.{u_1, u_4} (β := K) (SummationFilter.unconditional α).filter
  (fun (x : Finset α) ↦ (∏ b ∈ x, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)) fun (s : Finset α) ↦
  ∏ b ∈ s, g b
Tactic: classical
  refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
  filter_upwards [eventually_ge_atTop s] with t ht
  calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
refine :
  EventuallyEq.{u_1, u_4} (β := K) (SummationFilter.unconditional α).filter
    (fun (x : Finset α) ↦ (∏ b ∈ x, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)) fun (s : Finset α) ↦
    ∏ b ∈ s, g b
⊢ HasProd g (c * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i))
have h : ∀ (t : Finset α) (ht : s ≤ t), (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
Tactic: classical
  refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
  filter_upwards [eventually_ge_atTop s] with t ht
  calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
⊢ Multipliable g
have obtain : ∀ (c : K) (hc : HasProd f c), Multipliable g
Tactic: obtain ⟨c, hc⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
⊢ Multipliable g
have obtain : ∀ (s : Finset α) (hs : ∀ i ∉ s, f i = g i), Multipliable g
Tactic: obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
⊢ Multipliable g
have obtain : ∀ (c : K) (hc : HasProd f c), Multipliable g
Tactic: classical
  obtain ⟨c, hc⟩ := hf
  obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
  exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
obtain : ∀ (c : K) (hc : HasProd f c), Multipliable g
⊢ Multipliable g
have obtain₁ : ∀ (c : K) (hc : HasProd f c) (s : Finset α) (hs : ∀ i ∉ s, f i = g i), Multipliable g
Tactic: classical
  obtain ⟨c, hc⟩ := hf
  obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
  exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
have mp : Summable f →
  (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
mp :
  Summable f →
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
have mpr : (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i)) →
  Summable f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable f
have mpr : Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) ∧
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
Tactic: apply (summable_iff_summable_compl_and_tsum_mem f).mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
have mpr : Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f)
have mpr : CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
  ∑ b ∈ s, ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) b
Tactic: apply summable_iff_cauchySeq_finset.mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    ∑ b ∈ s, ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) b
have mpr : CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
  (toCompl : (a : α) → UniformSpace.Completion α) (∑ x ∈ s, f x)
Tactic: simp_rw [Function.comp_apply, ← map_sum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
have mp : Summable f →
  (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
Tactic: classical
  constructor
  · rintro ⟨a, ha⟩
    exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩
  · rintro ⟨h_cauchy, h_tsum⟩
    apply (summable_iff_summable_compl_and_tsum_mem f).mpr
    constructor
    · apply summable_iff_cauchySeq_finset.mpr
      simp_rw [Function.comp_apply, ← map_sum]
      exact h_cauchy.map (uniformContinuous_coe α)
    · exact h_tsum
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
mp :
  Summable f →
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
have mpr : (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i)) →
  Summable f
Tactic: classical
  constructor
  · rintro ⟨a, ha⟩
    exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩
  · rintro ⟨h_cauchy, h_tsum⟩
    apply (summable_iff_summable_compl_and_tsum_mem f).mpr
    constructor
    · apply summable_iff_cauchySeq_finset.mpr
      simp_rw [Function.comp_apply, ← map_sum]
      exact h_cauchy.map (uniformContinuous_coe α)
    · exact h_tsum
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
⊢ ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)
have inl : ∑'[L] (i : β), HSMul.hSMul.{u_5, u_1, u_1} (α := γ) 0 (f i) =
  HSMul.hSMul.{u_5, u_1, u_1} (α := γ) (β := α) 0 (∑'[L] (i : β), f i)
Tactic: rcases eq_or_ne g 0 with rfl | hg
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
inl :
  ∑'[L] (i : β), HSMul.hSMul.{u_5, u_1, u_1} (α := γ) 0 (f i) =
    HSMul.hSMul.{u_5, u_1, u_1} (α := γ) (β := α) 0 (∑'[L] (i : β), f i)
⊢ ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)
have inr : ∀ (hg : g ≠ 0), ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)
Tactic: rcases eq_or_ne g 0 with rfl | hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ ((e : (a : M) → M₂) (f b) : M₂)) ((e : (a : M) → M₂) x : M₂) L ↔
    HasSum f x L
have rw : HasSum f ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) x : M₂)) L ↔ HasSum f x L
Tactic: rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
rw : HasSum f ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) x : M₂)) L ↔ HasSum f x L
⊢ HasSum.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ ((e : (a : M) → M₂) (f b) : M₂)) ((e : (a : M) → M₂) x : M₂) L ↔
    HasSum f x L
have rw₁ : HasSum f x L ↔ HasSum f x L
Tactic: rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have pos : ∀ (hf : Summable f L),
  ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: by_cases hf : Summable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
pos :
  ∀ (hf : Summable f L),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have neg : ∀ (hf : ¬Summable f L),
  ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: by_cases hf : Summable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have pos : ∀ (hL : L.NeBot),
  ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
pos :
  ∀ (hL : L.NeBot),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have neg : ∀ (hL : ¬L.NeBot),
  ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have neg : ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y ↔ (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
Tactic: simp only [tsum_bot hL, eq_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y ↔ (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
have neg : ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y → (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
neg : ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y → (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
⊢ ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y ↔ (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
have neg₁ : (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y → ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (hypothesis)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
Tactic: have hf' : ¬Summable (fun z ↦ e (f z)) L := fun h ↦ hf (e.summable.mp h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
have neg : 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
⊢ 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
have neg : 0 = y → Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
Tactic: refine ⟨?_, fun H ↦ ?_⟩