awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
pos : ∀ (H : ∃ (x : M), x ≠ 0 ∧ x ∈ W), IsOpen[inst_1] {0}
⊢ IsOpen[inst_1] {0}
have neg : ∀ (H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W), IsOpen[inst_1] {0}
Tactic: by_cases H : ∃ x ≠ 0, x ∈ W
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ∃ (x : M), x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst_1] {0}
have pos : ∀ (x : M) (hx : x ≠ 0) (hxW : x ∈ W), IsOpen[inst_1] {0}
Tactic: obtain ⟨x, hx, hxW⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst_1] {0}
have hW₁ : Membership.mem (γ := Filter M) (𝓝 0) {0}
Tactic: obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
Cleared hypotheses: W, hW, hW', H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
hW₁ : Membership.mem (γ := Filter M) (𝓝 0) {0}
⊢ IsOpen[inst_1] {0}
have hW'₁ : HMul.hMul (α := Set M) univ {0} ⊆ U
Tactic: obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
Cleared hypotheses: W, hW, hW', H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
hW₁ : Membership.mem (γ := Filter M) (𝓝 0) {0}
hW'₁ : HMul.hMul (α := Set M) univ {0} ⊆ U
⊢ IsOpen[inst_1] {0}
have H₁ : ¬∃ (x : M), x ≠ 0 ∧ Membership.mem (γ := Set M) {0} x
Tactic: obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
Cleared hypotheses: W, hW, hW', H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 1) s
⊢ ∃ (V : Set M), IsOpen[inst] V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
have this : Membership.mem (γ := Filter (M × M)) (𝓝 (1, 1)) ((fun (a : M × M) ↦ a.1 * a.2) ⁻¹' s)
Tactic: have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
    tendsto_mul (by simpa only [one_mul] using hs)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : HasBasis (𝓝 1) p s
⊢ HasBasis.{u_3, u_1 + 1} (α := M) (𝓝 1) p fun (i : ι) ↦ s i * s i
have rw : HasBasis (α := M)
  (Filter.map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))) p
  fun (i : ι) ↦ s i * s i
Tactic: rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx) :
      M)
have refine_1 : ∀ (x : M), Continuous[inst_1, inst_1] (HMul.hMul x)
Tactic: refine eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
refine_1 : ∀ (x : M), Continuous[inst_1, inst_1] (HMul.hMul x)
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx) :
      M)
have refine_2 : ∀ (y : M), Continuous[inst_1, inst_1] fun (x : M) ↦ x * y
Tactic: refine eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
N : Type u_4
inst : TopologicalSpace N
inst_1 : Mul N
inst_2 : ContinuousMul N
s t : Set N
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)
have rw : IsCompact (X := N) ((fun (x : N × N) ↦ x.1 * x.2) '' s ×ˢ t)
Tactic: rw [← image_mul_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun (x : M) ↦ a * x) (cocompact M) (cocompact M)
have refine : Tendsto ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) (cocompact M) (cocompact M)
Tactic: refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_const_mul b))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) (cocompact M) (cocompact M)
have h : Eq.{u_3 + 1} (α := M → M) ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) id
Tactic: convert! Filter.tendsto_id
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Eq.{u_3 + 1} (α := M → M) ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) id
have h : ∀ (x : M), ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) x = id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun (x : M) ↦ x * a) (cocompact M) (cocompact M)
have refine : Tendsto ((fun (x : M) ↦ x * b) ∘ fun (x : M) ↦ x * a) (cocompact M) (cocompact M)
Tactic: refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_const b))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun (x : M) ↦ x * b) ∘ fun (x : M) ↦ x * a) (cocompact M) (cocompact M)
have simp : Tendsto (fun (x : M) ↦ x) (cocompact M) (cocompact M)
Tactic: simp only [comp_mul_right, ha, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
have rcases : ∀ (W : Set M) (W1 : Membership.mem (γ := Filter M) (𝓝 1) W) (h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u),
  ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
Tactic: rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
W : Set M
W1 : Membership.mem (γ := Filter M) (𝓝 1) W
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
have rcases : ∀ (V : Set M) (V1 : Membership.mem (γ := Filter M) (𝓝 1) V) (h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W),
  ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
Tactic: rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
W : Set M
W1 : Membership.mem (γ := Filter M) (𝓝 1) W
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : Membership.mem (γ := Filter M) (𝓝 1) V
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
have right : ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
Tactic: use V, V1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
f_1 : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ i ∈ f :: l, Tendsto (f_1 i) x (𝓝 (a i))
⊢ Tendsto (fun (b : α) ↦ List.prod (List.map (fun (c : ι) ↦ f_1 c b) (f :: l))) x (𝓝 (List.map a (f :: l)).prod)
have simp : Tendsto (fun (b : α) ↦ f_1 f b * List.prod (List.map (fun (c : ι) ↦ f_1 c b) l)) x (𝓝 (a f * (List.map a l).prod))
Tactic: simp only [List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt.{u_5, u_3} (Y := M) (fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l)) t x
have rw : ContinuousAt.{u_5, u_3} (Y := M)
  (t.restrict (π := fun (a : X) ↦ M) fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l))
  (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
Tactic: rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt.{u_5, u_3} (Y := M)
    (t.restrict (π := fun (a : X) ↦ M) fun (a : X) ↦ List.prod (List.map (fun (i : ι) ↦ f i a) l))
    (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
have refine : ∀ (i : ι) (hi : i ∈ l),
  Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
    (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))
Tactic: refine tendsto_list_prod _ fun i hi => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
    (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))
have h₁ : ContinuousWithinAt (f i) t x
Tactic: specialize h i hi x hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ Tendsto (fun (b : (↑t : Type u_5)) ↦ f i (↑b : X)) (𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx))
    (𝓝 (f i (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx) : X)))
have h₁ : ContinuousAt (t.restrict (π := fun (a : X) ↦ M) (f i)) (Subtype.mk (p := fun (x : X) ↦ x ∈ t) x hx)
Tactic: rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
k : ℕ
⊢ Continuous[inst, inst] fun (a : M) ↦ a ^ (k + 1)
have simp : Continuous[inst, inst] fun (a : M) ↦ a * a ^ k
Tactic: simp only [pow_succ']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : IsScalarTower R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ q • x
have simp : Continuous[inst_7, inst_7] fun (x : A) ↦ HSMul.hSMul (β := A) q 1 * x
Tactic: simp +singlePass only [← smul_one_mul q (_ : A)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Monoid M
inst_3 : ContinuousMul M
R : Type u_6
A : Type u_7
inst_4 : Monoid A
inst_5 : SMul R A
inst_6 : SMulCommClass R A A
inst_7 : TopologicalSpace A
inst_8 : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst_7, inst_7] fun (x : A) ↦ q • x
have simp : Continuous[inst_7, inst_7] fun (x : A) ↦ x * HSMul.hSMul (β := A) q 1
Tactic: simp +singlePass only [← mul_smul_one q (_ : A)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
inst : TopologicalSpace M
inst_1 : CommMonoid M
inst_2 : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun (b : α) ↦ Multiset.prod (Multiset.map (fun (c : ι) ↦ f c b) s)) x (𝓝 (Multiset.map a s).prod)
have mk : ∀ (l : List ι),
  (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        Tendsto (f i) x (𝓝 (a i))) →
    Tendsto
      (fun (b : α) ↦
        Multiset.prod (Multiset.map (fun (c : ι) ↦ f c b) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
      x (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod)
Tactic: rcases s with ⟨l⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
s : Multiset ι
⊢ (∀ i ∈ s, Continuous[inst, inst_1] (f i)) →
    Continuous[inst, inst_1] fun (a : X) ↦ Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) s)
have mk : ∀ (l : List ι),
  (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        Continuous[inst, inst_1] (f i)) →
    Continuous[inst, inst_1] fun (a : X) ↦
      Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
Tactic: rcases s with ⟨l⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ i ∈ s, ContinuousOn (f i) t) →
    ContinuousOn.{u_5, u_3} (Y := M) (fun (a : X) ↦ Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) s)) t
have mk : ∀ (l : List ι),
  (∀ (i : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i →
        ContinuousOn (f i) t) →
    ContinuousOn.{u_5, u_3} (Y := M)
      (fun (a : X) ↦
        Multiset.prod (Multiset.map (fun (i : ι) ↦ f i a) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)))
      t
Tactic: rcases s with ⟨l⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
have rwa : ∀ i ∈ s, ∀ᶠ (x : X) in l, f i x = g i x
Tactic: rwa [eventually_all_finset]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ EventuallyEq.{u_6, u_7} (β := M) l (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have hs₁ : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
Tactic: replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x := by rwa [eventually_all_finset]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
X : Type u_6
M : Type u_7
inst : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
⊢ EventuallyEq.{u_6, u_7} (β := M) l (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have h : ∀ (x : X) (hx : ∀ i ∈ s, f i x = g i x), Eq.{u_7 + 1} (α := M) ((∏ i ∈ s, f i) x) ((∏ i ∈ s, g i) x)
Tactic: filter_upwards [hs] with x hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : One M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x₀ : X
⊢ ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)
have rcases : ∀ (U : Set X) (hxU : U ∈ 𝓝 x₀)
  (hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}),
  ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)
Tactic: rcases hf x₀ with ⟨U, hxU, hUf⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : One M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}
⊢ ∃ (I : Finset ι), ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i x) ⊆ (↑I : Set ι)
have refine : ∀ (y : X) (hy : y ∈ U) (i : ι)
  (hi : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i y) i),
  i ∈ (↑(hUf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty})) : Set ι)
Tactic: refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
X : Type u_5
inst : TopologicalSpace X
M : Type u_6
inst_1 : One M
f : ι → X → M
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite.{u_1} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty}
y : X
hy : y ∈ U
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_6} (M := M) fun (i : ι) ↦ f i y) i
⊢ i ∈ (↑(hUf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty})) : Set ι)
have rw : Membership.mem (γ := Set ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ U).Nonempty} i
Tactic: rw [hUf.coe_toFinset]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (i : ι), f i x
have refine : ∀ (x : X), ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
Tactic: refine continuous_iff_continuousAt.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
have rcases : ∀ (s : Finset ι) (hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)),
  ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
Tactic: rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, Eq.{u_3 + 1} (α := M) (∏ᶠ (i : ι), f i y) (∏ i ∈ s, f i y)
⊢ ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ᶠ (i : ι), f i x) x
have refine : ContinuousAt.{u_5, u_3} (Y := M) (fun (x : X) ↦ ∏ i ∈ s, f i x) x
Tactic: refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
M : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst, inst_1] (f i)
hf : LocallyFinite.{u_1, u_5} (X := X) fun (i : ι) ↦ mulSupport (f i)
⊢ Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (i : ι) (_ : p i), f i x
have simp : Continuous[inst, inst_1] fun (x : X) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x
Tactic: simp only [← finprod_subtype_eq_finprod_cond]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
have rw : ContinuousMul M
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
have refine : ∀ (b : Bool), ContinuousMul M
Tactic: refine continuousMul_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
have false : ContinuousMul M
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
false : ContinuousMul M
⊢ ContinuousMul M
have true : ContinuousMul M
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y : X
⊢ Eq (α := C(X, X)) (ContinuousMap.mulRight (x * y)) (comp (ContinuousMap.mulRight y) (ContinuousMap.mulRight x))
have h : ∀ (a : X),
  Eq (α := X) ((ContinuousMap.mulRight (x * y) : (a : X) → X) a : X)
    ((comp (ContinuousMap.mulRight y) (ContinuousMap.mulRight x) : (a : X) → X) a : X)
Tactic: ext