awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this : ContinuousAdd N
⊢ Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have eq_moduleTopology' : LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
Tactic: refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
⊢ LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have this₁ : IsModuleTopology R P
Tactic: have : IsModuleTopology R P := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this : IsModuleTopology R P
⊢ LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have this₁ : ContinuousAdd P
Tactic: have : ContinuousAdd P := ModuleTopology.continuousAdd R P
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this_3 : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
⊢ LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have eq_moduleTopology' : Continuous (X := M × N) id
Tactic: rw [← continuous_id_iff_le]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this_3 : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ i = (fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2)
have h : ∀ (a : M) (b : N),
  (i (a, b)).1 =
    (((fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2))
        (a, b)).1
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this_3 : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
h :
  ∀ (a : M) (b : N),
    (i (a, b)).1 =
      (((fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2))
          (a, b)).1
⊢ i = (fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2)
have h₁ : ∀ (a : M) (b : N),
  (i (a, b)).2 =
    (((fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2))
        (a, b)).2
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this_3 : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous i
have eq_moduleTopology' : Continuous (X := M × N) (Y := P)
  ((fun (abcd : P × P) ↦ abcd.1 + abcd.2) ∘ fun (ab : M × N) ↦ ((i₁ : (a : M) → P) ab.1, (i₂ : (a : N) → P) ab.2))
Tactic: rw [show (i : M × N → P) =
       (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘
       (fun ab ↦ (i₁ ab.1, i₂ ab.2)) by
       ext ⟨a, b⟩ <;> aesop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
A : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (A i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (A i)
inst_5 : (i : ι) → TopologicalSpace (A i)
inst_6 : ∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)
⊢ IsModuleTopology R ((i : ι) → A i)
have of_equiv : ∀ {α β : Type u_2} (a : α ≃ β),
  (∀ {A : α → Type u_3} [inst_7 : (i : α) → AddCommMonoid (A i)] [inst_8 : (i : α) → Module.{u_1, u_3} R (A i)]
      [inst_9 : (i : α) → TopologicalSpace (A i)] [∀ (i : α), IsModuleTopology.{u_1, u_3} R (A i)],
      IsModuleTopology R ((i : α) → A i)) →
    ∀ {A : β → Type u_3} [inst_7 : (i : β) → AddCommMonoid (A i)] [inst_8 : (i : β) → Module.{u_1, u_3} R (A i)]
      [inst_9 : (i : β) → TopologicalSpace (A i)] [∀ (i : β), IsModuleTopology.{u_1, u_3} R (A i)],
      IsModuleTopology R ((i : β) → A i)
Tactic: induction ι using Finite.induction_empty_option
Cleared hypotheses: A, inst_3, inst_4, inst_5, inst_6
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
A : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (A i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (A i)
inst_5 : (i : ι) → TopologicalSpace (A i)
inst_6 : ∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)
of_equiv :
  ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {A : α → Type u_3} [inst_7 : (i : α) → AddCommMonoid (A i)] [inst_8 : (i : α) → Module.{u_1, u_3} R (A i)]
        [inst_9 : (i : α) → TopologicalSpace (A i)] [∀ (i : α), IsModuleTopology.{u_1, u_3} R (A i)],
        IsModuleTopology R ((i : α) → A i)) →
      ∀ {A : β → Type u_3} [inst_7 : (i : β) → AddCommMonoid (A i)] [inst_8 : (i : β) → Module.{u_1, u_3} R (A i)]
        [inst_9 : (i : β) → TopologicalSpace (A i)] [∀ (i : β), IsModuleTopology.{u_1, u_3} R (A i)],
        IsModuleTopology R ((i : β) → A i)
⊢ IsModuleTopology R ((i : ι) → A i)
have h_empty : ∀ {A : PEmpty.{u_2 + 1} → Type u_3} [inst_7 : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)]
  [inst_8 : (i : PEmpty.{u_2 + 1}) → Module.{u_1, u_3} R (A i)]
  [inst_9 : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)]
  [∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology.{u_1, u_3} R (A i)], IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)
Tactic: induction ι using Finite.induction_empty_option
Cleared hypotheses: A, inst_3, inst_4, inst_5, inst_6
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
A : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (A i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (A i)
inst_5 : (i : ι) → TopologicalSpace (A i)
inst_6 : ∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)
of_equiv :
  ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {A : α → Type u_3} [inst_7 : (i : α) → AddCommMonoid (A i)] [inst_8 : (i : α) → Module.{u_1, u_3} R (A i)]
        [inst_9 : (i : α) → TopologicalSpace (A i)] [∀ (i : α), IsModuleTopology.{u_1, u_3} R (A i)],
        IsModuleTopology R ((i : α) → A i)) →
      ∀ {A : β → Type u_3} [inst_7 : (i : β) → AddCommMonoid (A i)] [inst_8 : (i : β) → Module.{u_1, u_3} R (A i)]
        [inst_9 : (i : β) → TopologicalSpace (A i)] [∀ (i : β), IsModuleTopology.{u_1, u_3} R (A i)],
        IsModuleTopology R ((i : β) → A i)
h_empty :
  ∀ {A : PEmpty.{u_2 + 1} → Type u_3} [inst_7 : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)]
    [inst_8 : (i : PEmpty.{u_2 + 1}) → Module.{u_1, u_3} R (A i)]
    [inst_9 : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology.{u_1, u_3} R (A i)], IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)
⊢ IsModuleTopology R ((i : ι) → A i)
have h_option : ∀ {α : Type u_2} [Fintype α],
  (∀ {A : α → Type u_3} [inst_8 : (i : α) → AddCommMonoid (A i)] [inst_9 : (i : α) → Module.{u_1, u_3} R (A i)]
      [inst_10 : (i : α) → TopologicalSpace (A i)] [∀ (i : α), IsModuleTopology.{u_1, u_3} R (A i)],
      IsModuleTopology R ((i : α) → A i)) →
    ∀ {A : Option α → Type u_3} [inst_8 : (i : Option α) → AddCommMonoid (A i)]
      [inst_9 : (i : Option α) → Module.{u_1, u_3} R (A i)] [inst_10 : (i : Option α) → TopologicalSpace (A i)]
      [∀ (i : Option α), IsModuleTopology.{u_1, u_3} R (A i)], IsModuleTopology R ((i : Option α) → A i)
Tactic: induction ι using Finite.induction_empty_option
Cleared hypotheses: A, inst_3, inst_4, inst_5, inst_6
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι_1 : Type u_2
inst_2 : Finite ι_1
ι : Type u_2
inst_3 : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst_8 : (i : ι) → AddCommMonoid (A i)] [inst_9 : (i : ι) → Module.{u_1, u_3} R (A i)]
    [inst_10 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst_4 : (i : Option ι) → AddCommMonoid (A i)
inst_5 : (i : Option ι) → Module.{u_1, u_3} R (A i)
inst_6 : (i : Option ι) → TopologicalSpace (A i)
inst_7 : ∀ (i : Option ι), IsModuleTopology.{u_1, u_3} R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
⊢ IsModuleTopology R ((i : Option ι) → A i)
have suffices : IsModuleTopology R ((i' : ι ⊕ Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) i'))
Tactic: suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from
      .iso (.piCongrLeft R A e.symm)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι_1 : Type u_2
inst_2 : Finite ι_1
ι : Type u_2
inst_3 : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst_8 : (i : ι) → AddCommMonoid (A i)] [inst_9 : (i : ι) → Module.{u_1, u_3} R (A i)]
    [inst_10 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst_4 : (i : Option ι) → AddCommMonoid (A i)
inst_5 : (i : Option ι) → Module.{u_1, u_3} R (A i)
inst_6 : (i : Option ι) → TopologicalSpace (A i)
inst_7 : ∀ (i : Option ι), IsModuleTopology.{u_1, u_3} R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
⊢ IsModuleTopology R ((i' : ι ⊕ Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) i'))
have suffices : IsModuleTopology R
  (((s : ι) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inl s))) ×
    ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t))))
Tactic: suffices IsModuleTopology R
      (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t)))) from
      .iso (ContinuousLinearEquiv.sumPiEquivProdPi R ι Unit _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι_1 : Type u_2
inst_2 : Finite ι_1
ι : Type u_2
inst_3 : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst_8 : (i : ι) → AddCommMonoid (A i)] [inst_9 : (i : ι) → Module.{u_1, u_3} R (A i)]
    [inst_10 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology.{u_1, u_3} R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst_4 : (i : Option ι) → AddCommMonoid (A i)
inst_5 : (i : Option ι) → Module.{u_1, u_3} R (A i)
inst_6 : (i : Option ι) → TopologicalSpace (A i)
inst_7 : ∀ (i : Option ι), IsModuleTopology.{u_1, u_3} R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
⊢ IsModuleTopology R
    (((s : ι) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inl s))) ×
      ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t))))
have this : IsModuleTopology.{u_1, u_3} R ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t)))
Tactic: have :=
      IsModuleTopology.iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
⊢ Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have intro : ∀ (val : Fintype ι),
  Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
⊢ Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
have h : ∀ (f : ι → R) (b : B),
  Eq.{u_3 + 1} (α := C) ((((bil : (a : ι → R) → B →ₗ[R] C) (f, b).1 : B →ₗ[R] C) : (a : B) → C) (f, b).2 : C)
    (∑ i : ι,
        HSMul.hSMul (β := C) ((f, b).1 i)
          ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C)
              (f, b).2 :
            C) :
      C)
Tactic: ext ⟨f, b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
f : ι → R
b : B
⊢ Eq.{u_3 + 1} (α := C) ((((bil : (a : ι → R) → B →ₗ[R] C) (f, b).1 : B →ₗ[R] C) : (a : B) → C) (f, b).2 : C)
    (∑ i : ι,
        HSMul.hSMul (β := C) ((f, b).1 i)
          ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C)
              (f, b).2 :
            C) :
      C)
have h : Eq.{u_3 + 1} (α := C)
  (((bil : (a : ι → R) → B →ₗ[R] C) (∑ i : ι, Pi.single (M := fun (i : ι) ↦ R) i (f i), b).1 : (a : B) → C) (f, b).2 :
    C)
  (∑ i : ι,
      HSMul.hSMul (β := C) ((f, b).1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) (f, b).2 :
          C) :
    C)
Tactic: nth_rw 1 [← Finset.univ_sum_single f]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
f : ι → R
b : B
⊢ Eq.{u_3 + 1} (α := C)
    (((bil : (a : ι → R) → B →ₗ[R] C) (∑ i : ι, Pi.single (M := fun (i : ι) ↦ R) i (f i), b).1 : (a : B) → C) (f, b).2 :
      C)
    (∑ i : ι,
        HSMul.hSMul (β := C) ((f, b).1 i)
          ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C)
              (f, b).2 :
            C) :
      C)
have h : Eq.{u_3 + 1} (α := C)
  (∑ c : ι, (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single c (f c)) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b)
  (∑ x : ι,
    HSMul.hSMul (β := C) (f x)
      ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C))
Tactic: simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coe_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
f : ι → R
b : B
⊢ Eq.{u_3 + 1} (α := C)
    (∑ c : ι, (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single c (f c)) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b)
    (∑ x : ι,
      HSMul.hSMul (β := C) (f x)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C))
have h : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x (f x)) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b =
      HSMul.hSMul (β := C) (f x)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C)
Tactic: refine Finset.sum_congr rfl (fun x _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
f : ι → R
b : B
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x (f x)) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b =
    HSMul.hSMul (β := C) (f x)
      ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C)
have h : (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(HSMul.hSMul (β := ι →₀ R) (f x) (Finsupp.single x 1)) : (a : ι) → R) : B →ₗ[R] C) :
      (a : B) → C)
    b =
  HSMul.hSMul (β := C) (f x)
    ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C)
Tactic: rw [← Finsupp.smul_single_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
f : ι → R
b : B
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (((bil : (a : ι → R) → B →ₗ[R] C) (⇑(HSMul.hSMul (β := ι →₀ R) (f x) (Finsupp.single x 1)) : (a : ι) → R) :
          B →ₗ[R] C) :
        (a : B) → C)
      b =
    HSMul.hSMul (β := C) (f x)
      ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C)
have h : (((bil : (a : ι → R) → B →ₗ[R] C) (HSMul.hSMul (β := (a : ι) → R) (f x) (⇑(Finsupp.single x 1) : (a : ι) → R)) :
        B →ₗ[R] C) :
      (a : B) → C)
    b =
  HSMul.hSMul (β := C) (f x)
    ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single x 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) b : C)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
⊢ Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have h : Eq (α := (fb : (ι → R) × B) → C)
  (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
  fun (fb : (ι → R) × B) ↦
  ∑ i : ι,
    HSMul.hSMul (β := C) (fb.1 i)
      ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
Tactic: have h : (fun fb ↦ bil fb.1 fb.2 : ((ι → R) × B → C)) =
      (fun fb ↦ ∑ i, ((fb.1 i) • (bil (Finsupp.single i 1) fb.2) : C)) := by
    ext ⟨f, b⟩
    nth_rw 1 [← Finset.univ_sum_single f]
    simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coe_sum, Finset.sum_apply]
    refine Finset.sum_congr rfl (fun x _ ↦ ?_)
    rw [← Finsupp.smul_single_one]
    push_cast
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
h :
  Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
⊢ Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have intro : Continuous (Y := C) fun (fb : (ι → R) × B) ↦
  ∑ i : ι,
    HSMul.hSMul (β := C) (fb.1 i)
      ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
Tactic: rw [h]