awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (hypothesis)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
h : Tendsto.{u_3, u_3} (α := G₀) Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x
have hx' : x⁻¹ ≠ 0
Tactic: have hx' := inv_ne_zero hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
h : Tendsto.{u_3, u_3} (α := G₀) Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ ContinuousAt Inv.inv x
have rw : Tendsto.{u_3, u_3} (α := G₀) (β := G₀) ((fun (x_1 : G₀) ↦ x_1 * x⁻¹⁻¹) ∘ Inv.inv ∘ fun (x_1 : G₀) ↦ x * x_1) (𝓝 1) (𝓝 1)
Tactic: rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
      tendsto_map'_iff, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ m) x
have ofNat : ∀ (m : ℕ) (h : x ≠ 0 ∨ 0 ≤ Int.ofNat m), ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.ofNat m) x
Tactic: rcases m with m | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
ofNat : ∀ (m : ℕ) (h : x ≠ 0 ∨ 0 ≤ Int.ofNat m), ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.ofNat m) x
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ m) x
have negSucc : ∀ (m : ℕ) (h : x ≠ 0 ∨ 0 ≤ Int.negSucc m), ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.negSucc m) x
Tactic: rcases m with m | m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ x ^ Int.negSucc m) x
have negSucc : ContinuousAt (Y := G₀) (fun (x : G₀) ↦ (x ^ (m + 1))⁻¹) x
Tactic: simp only [zpow_negSucc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (hypothesis)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (Y := G₀) (fun (x : G₀) ↦ (x ^ (m + 1))⁻¹) x
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_ge
-- Lean 4 proof step from Mathlib.Topology.Algebra.Indicator (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∉ frontier s
⊢ ContinuousAt (s.mulIndicator f) x
have hx₁ : x ∈ interior s ∪ interior sᶜ
Tactic: rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x
have inl : ∀ (h : x ∈ interior s), ContinuousAt (s.mulIndicator f) x
Tactic: obtain h | h := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
inl : ∀ (h : x ∈ interior s), ContinuousAt (s.mulIndicator f) x
⊢ ContinuousAt (s.mulIndicator f) x
have inr : ∀ (h : x ∈ interior sᶜ), ContinuousAt (s.mulIndicator f) x
Tactic: obtain h | h := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Indicator (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ ContinuousAt (s.mulIndicator f) x
have hs : interior s ∈ 𝓝 x
Tactic: have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior])
-- 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 α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a
have rw : ∀ x ∉ Set.range g, extend g f 1 x = 1
Tactic: rw [← hg.hasProd_iff, extend_comp hg]
-- 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 : α
s : Set β
⊢ HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔ HasProd (s.mulIndicator f) a
have rw : HasProd (β := (↑s : Type u_2))
    (Set.mulIndicator (Set.range (ι := (↑s : Type u_2)) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) f ∘
      Subtype.val (p := fun (x : β) ↦ x ∈ s))
    a ↔
  HasProd (s.mulIndicator f) a
Tactic: rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]
-- 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 : α
s : Set β
rw :
  HasProd (β := (↑s : Type u_2))
      (Set.mulIndicator (Set.range (ι := (↑s : Type u_2)) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) f ∘
        Subtype.val (p := fun (x : β) ↦ x ∈ s))
      a ↔
    HasProd (s.mulIndicator f) a
⊢ HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔ HasProd (s.mulIndicator f) a
have rw₁ : HasProd (β := (↑s : Type u_2)) (s.mulIndicator f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔
  HasProd (s.mulIndicator f) a
Tactic: rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]
-- 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 : α
s : Set β
rw :
  HasProd (β := (↑s : Type u_2))
      (Set.mulIndicator (Set.range (ι := (↑s : Type u_2)) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) f ∘
        Subtype.val (p := fun (x : β) ↦ x ∈ s))
      a ↔
    HasProd (s.mulIndicator f) a
rw₁ :
  HasProd (β := (↑s : Type u_2)) (s.mulIndicator f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔
    HasProd (s.mulIndicator f) a
⊢ HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔ HasProd (s.mulIndicator f) a
have rw₂ : HasProd (s.mulIndicator f) a ↔ HasProd (s.mulIndicator f) a
Tactic: rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
have this : Multipliable (β := (↑(↑(hs.toFinset (s := s)) : Set β) : Type u_2))
  (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑(hs.toFinset (s := s)) : Set β)))
Tactic: have := hs.toFinset.multipliable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this :
  Multipliable (β := (↑(↑(hs.toFinset (s := s)) : Set β) : Type u_2))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑(hs.toFinset (s := s)) : Set β)))
⊢ Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
have rwa : ∀ (this : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))),
  Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
Tactic: rwa [hs.coe_toFinset] 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 : β → α
L : SummationFilter β
inst_2 : L.HasSupport
h : HasFiniteMulSupport f
⊢ Multipliable f L
have hf : ∀ b ∉ Set.Finite.toFinset (s := mulSupport f) h, f b = 1
Tactic: apply multipliable_of_ne_finset_one (s := h.toFinset)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
inst_2 : DecidablePred fun (x : β) ↦ x = b
a : α
L : SummationFilter β
inst_3 : L.LeAtTop
⊢ HasProd (fun (b' : β) ↦ if b' = b then a else 1) a L
have h : a = if b = b then a else 1
Tactic: convert! hasProd_single b (hf := fun b' hb' ↦ if_neg hb') (L := L)
-- 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 α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
⊢ HasProd f a ↔ HasProd g a
have this : Eq (α := (↑(mulSupport f) : Type u_2) → α)
  (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
    (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
  (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
Tactic: have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
-- 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 α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
this :
  Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
⊢ HasProd f a ↔ HasProd g a
have rw : HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd g a
Tactic: rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]
-- 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 α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
this :
  Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
rw : HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd g a
⊢ HasProd f a ↔ HasProd g a
have rw₁ : HasProd.{u_1, u_2} (β := (↑(mulSupport f) : Type u_2))
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    a ↔
  HasProd g a
Tactic: rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]
-- 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 α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
this :
  Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
rw : HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd g a
rw₁ :
  HasProd.{u_1, u_2} (β := (↑(mulSupport f) : Type u_2))
      (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
        (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
      a ↔
    HasProd g a
⊢ HasProd f a ↔ HasProd g a
have rw₂ : HasProd (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g)) a ↔ HasProd g a
Tactic: rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]
-- 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 α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
this :
  Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
rw : HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd g a
rw₁ :
  HasProd.{u_1, u_2} (β := (↑(mulSupport f) : Type u_2))
      (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
        (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
      a ↔
    HasProd g a
rw₂ :
  HasProd (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g)) a ↔ HasProd g a
⊢ HasProd f a ↔ HasProd g a
have rw₃ : HasProd g a ↔ HasProd g a
Tactic: rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]
-- 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 α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
⊢ HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L
have this : Eq (α := Finset β → γ) (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
  fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b
Tactic: have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
    funext <| map_prod g _
-- 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 α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
this :
  Eq (α := Finset β → γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
    fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b
⊢ Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ (∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b : γ)) L.filter
    (𝓝 ((g : (a : α) → γ) a) : Filter γ)
have rw : Tendsto.{u_2, u_3} (β := γ)
  (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b : Finset β → γ)
  L.filter (𝓝 ((g : (a : α) → γ) a) : Filter γ)
Tactic: rw [← this]
-- 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 γ
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
a : α
⊢ HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L ↔ HasProd f a L
have simp_rw : Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ ((g : (a : α) → γ) (∏ x ∈ s, f x) : γ)) L.filter
    (𝓝 ((g : (a : α) → γ) a) : Filter γ) ↔
  Tendsto (fun (s : Finset β) ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)
Tactic: simp_rw [HasProd, comp_apply, ← _root_.map_prod]
-- 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 α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
inst_6 : FunLike G' γ α
inst_7 : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (⇑g' : (a : γ) → α)
hinv : LeftInverse.{u_1 + 1, u_3 + 1} (α := α) (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ)
h : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
⊢ Multipliable f L
have this : Multipliable.{u_1, u_2} (α := α)
  (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) ((⇑g : (a : α) → γ) ∘ f)) L
Tactic: have := h.map _ hg'
-- 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 α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
inst_6 : FunLike G' γ α
inst_7 : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (⇑g' : (a : γ) → α)
hinv : LeftInverse.{u_1 + 1, u_3 + 1} (α := α) (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ)
h : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
this :
  Multipliable.{u_1, u_2} (α := α)
    (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) ((⇑g : (a : α) → γ) ∘ f)) L
⊢ Multipliable f L
have rwa : ∀
  (this :
    Multipliable (α := α) (comp.{u_1 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ) ∘ f) L),
  Multipliable f L
Tactic: rwa [← Function.comp_assoc, hinv.id] at this
Cleared hypotheses: this
-- 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 α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
inst_6 : FunLike G' γ α
inst_7 : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (⇑g' : (a : γ) → α)
hinv : LeftInverse.{u_1 + 1, u_3 + 1} (α := α) (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ)
h : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
this :
  Multipliable.{u_1, u_2} (α := α)
    (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) ((⇑g : (a : α) → γ) ∘ f)) L
rwa :
  ∀
    (this :
      Multipliable (α := α) (comp.{u_1 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ) ∘ f) L),
    Multipliable f L
⊢ Multipliable f L
have rwa₁ : ∀ (this : Multipliable (id ∘ f) L), Multipliable f L
Tactic: rwa [← Function.comp_assoc, hinv.id] at this
Cleared hypotheses: this
-- 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 : α) → α')
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
have pos : ∀ (hL : L.NeBot),
  Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[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_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 : α) → α')
pos :
  ∀ (hL : L.NeBot),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
have neg : ∀ (hL : ¬L.NeBot),
  Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[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_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
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
have pos : ∀ (h : Multipliable f L),
  Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
Tactic: by_cases h : Multipliable f L
-- 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
pos :
  ∀ (h : Multipliable f L),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
have neg : ∀ (h : ¬Multipliable f L),
  Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
Tactic: by_cases h : Multipliable f L
-- 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
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
have neg : ¬Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L
Tactic: rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]