awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
eq_moduleTopology' : Continuous (X := M × N) id
⊢ LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))

Tactic:
rw [← continuous_id_iff_le]

Premises used: continuous_id_iff_le
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
eq_moduleTopology' : Continuous i
⊢ Continuous (X := M × N) id

Tactic:
change @Continuous (M × N) P instTopologicalSpaceProd τP i

Premises used: Continuous
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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
⊢ 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)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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:
aesop
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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:
aesop
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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))
⊢ Continuous i

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]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 (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:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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)
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)
⊢ IsModuleTopology R ((i : ι) → A i)

Tactic:
induction ι using Finite.induction_empty_option

Premises used: Finite.induction_empty_option
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
X Y : Type u_2
e : X ≃ Y
h :
  ∀ {A : X → Type u_3} [inst_7 : (i : X) → AddCommMonoid (A i)] [inst_8 : (i : X) → Module.{u_1, u_3} R (A i)]
    [inst_9 : (i : X) → TopologicalSpace (A i)] [∀ (i : X), IsModuleTopology.{u_1, u_3} R (A i)],
    IsModuleTopology R ((i : X) → A i)
A : Y → Type u_3
inst_3 : (i : Y) → AddCommMonoid (A i)
inst_4 : (i : Y) → Module.{u_1, u_3} R (A i)
inst_5 : (i : Y) → TopologicalSpace (A i)
inst_6 : ∀ (i : Y), IsModuleTopology.{u_1, u_3} R (A i)
⊢ IsModuleTopology R ((i : Y) → A i)

Tactic:
.iso (ContinuousLinearEquiv.piCongrLeft R A e)

Premises used: IsModuleTopology.iso, ContinuousLinearEquiv.piCongrLeft
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
X Y : Type u_2
e : X ≃ Y
h :
  ∀ {A : X → Type u_3} [inst_7 : (i : X) → AddCommMonoid (A i)] [inst_8 : (i : X) → Module.{u_1, u_3} R (A i)]
    [inst_9 : (i : X) → TopologicalSpace (A i)] [∀ (i : X), IsModuleTopology.{u_1, u_3} R (A i)],
    IsModuleTopology R ((i : X) → A i)
A : Y → Type u_3
inst_3 : (i : Y) → AddCommMonoid (A i)
inst_4 : (i : Y) → Module.{u_1, u_3} R (A i)
inst_5 : (i : Y) → TopologicalSpace (A i)
inst_6 : ∀ (i : Y), IsModuleTopology.{u_1, u_3} R (A i)
⊢ IsModuleTopology R ((i : Y) → A i)

Tactic:
exact .iso (ContinuousLinearEquiv.piCongrLeft R A e)
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
inst_2 : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst_3 : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst_4 : (i : PEmpty.{u_2 + 1}) → Module.{u_1, u_3} R (A i)
inst_5 : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst_6 : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology.{u_1, u_3} R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 ι
suffices : IsModuleTopology R ((i' : ι ⊕ Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) i'))
⊢ IsModuleTopology R ((i : Option ι) → A i)

Tactic:
suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from
      .iso (.piCongrLeft R A e.symm)
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 ι
suffices :
  IsModuleTopology R
    (((s : ι) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inl s))) ×
      ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t))))
⊢ IsModuleTopology R ((i' : ι ⊕ Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) i'))

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
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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.{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
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 ι
this : IsModuleTopology.{u_1, u_3} R ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t)))
⊢ IsModuleTopology R
    (((s : ι) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inl s))) ×
      ((t : Unit) → A ((e.symm : (a : ι ⊕ Unit) → Option ι) (Sum.inr t))))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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
⊢ 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 :
  ∀ (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)
⊢ 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:
ext ⟨f, b⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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)
⊢ 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:
nth_rw 1 [← Finset.univ_sum_single f]

Premises used: Finset.univ_sum_single
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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))
⊢ 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:
simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coe_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, LinearMap.coe_sum, map_sum, Finsupp.single_eq_pi_single
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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))

Tactic:
Finset.sum_congr rfl (fun x _ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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
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)
⊢ 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:
refine Finset.sum_congr rfl (fun x _ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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_1 : Membership.mem (γ := Finset ι) Finset.univ x
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)
⊢ (((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:
rw [← Finsupp.smul_single_one]

Premises used: Finsupp.smul_single_one
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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_1 : Membership.mem (γ := Finset ι) Finset.univ x
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)
⊢ (((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:
push_cast
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
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 (β := (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:
simp