awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
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 (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 this : ContinuousAdd C
Tactic: haveI : ContinuousAdd C := toContinuousAdd R C
-- 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: classical
  cases nonempty_fintype ι
  -- The map in question, `(f, b) ↦ bil f b`, is easily checked to be equal to
  -- `(f, b) ↦ ∑ᵢ f i • bil (single i 1) b` where `single i 1 : ι → R` sends `i` to `1` and
  -- everything else to `0`.
  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
  rw [h]
  -- But this map is obviously continuous, because for a fixed `i`, `bil (single i 1)` is
  -- linear and thus continuous, and scalar multiplication and finite sums are continuous
  haveI : ContinuousAdd C := toContinuousAdd R C
  fun_prop
-- 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
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
have intro₁ : ∀ (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
Tactic: classical
  cases nonempty_fintype ι
  -- The map in question, `(f, b) ↦ bil f b`, is easily checked to be equal to
  -- `(f, b) ↦ ∑ᵢ f i • bil (single i 1) b` where `single i 1 : ι → R` sends `i` to `1` and
  -- everything else to `0`.
  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
  rw [h]
  -- But this map is obviously continuous, because for a fixed `i`, `bil (single i 1)` is
  -- linear and thus continuous, and scalar multiplication and finite sums are continuous
  haveI : ContinuousAdd C := toContinuousAdd R C
  fun_prop
-- 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
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
intro₁ :
  ∀ (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
⊢ 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 ι)
  (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 (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: classical
  cases nonempty_fintype ι
  -- The map in question, `(f, b) ↦ bil f b`, is easily checked to be equal to
  -- `(f, b) ↦ ∑ᵢ f i • bil (single i 1) b` where `single i 1 : ι → R` sends `i` to `1` and
  -- everything else to `0`.
  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
  rw [h]
  -- But this map is obviously continuous, because for a fixed `i`, `bil (single i 1)` is
  -- linear and thus continuous, and scalar multiplication and finite sums are continuous
  haveI : ContinuousAdd C := toContinuousAdd R C
  fun_prop
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have obtain : ∀ (m : ℕ) (f : (Fin m → R) →ₗ[R] A)
  (hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)),
  Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
Tactic: obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have hφ : Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)
Tactic: have hφ : Function.Surjective φ := Function.Surjective.prodMap hf fun b ↦ ⟨b, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have rw : Continuous (X := Prod.{u_1, u_3} (Fin m → R) B) (Y := C)
  ((fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2) ∘
    (⇑φ : (a : (Fin m → R) × B) → A × B))
Tactic: rw [Topology.IsQuotientMap.continuous_iff (isQuotientMap_of_surjective hφ)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Eq (α := (ab : A × B) → C) (fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2)
    ((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap)
have h : ∀ (x : A × B),
  Eq.{u_4 + 1} (α := C) ((((bil : (a : A) → B →ₗ[R] C) x.1 : B →ₗ[R] C) : (a : B) → C) x.2 : C)
    (((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
have rw : Continuous (X := A × B) (Y := C)
  ((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap)
Tactic: rw [show (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) =
    ((fun ba ↦ bil.flip ba.1 ba.2 : (B × A → C)) ∘ (Prod.swap : A × B → B × A)) by ext; simp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : MultilinearMap R M₁ M₂
hf : Continuous (f.toFun (M₁ := M₁))
g : MultilinearMap R M₁ M₂
hg : Continuous (g.toFun (M₁ := M₁))
h : (mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁) = (mk (M₁ := M₁) g hg).toMultilinearMap (M₁ := M₁)
⊢ mk (M₁ := M₁) f hf = mk (M₁ := M₁) g hg
have subst : ∀ (hg : Continuous ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁).toFun (M₁ := M₁))),
  mk (M₁ := M₁) f hf = mk (M₁ := M₁) ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁)) hg
Tactic: subst h
Cleared hypotheses: g, hg, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₃) (⇑(g.compContinuousMultilinearMap (M₁ := M₁) f) : (a : (i : ι) → M₁ i) → M₃)
    (comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂))
have h : ∀ (m : (i : ι) → M₁ i),
  Eq.{w₃ + 1} (α := M₃) ((g.compContinuousMultilinearMap (M₁ := M₁) f : (a : (i : ι) → M₁ i) → M₃) m : M₃)
    (comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) m : M₃)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
⊢ f = g ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g
have rw : f = g ↔
  (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f,
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f) =
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
Tactic: rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
rw :
  f = g ↔
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f) =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
⊢ f = g ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g
have rw₁ : f = g ↔
  (Equiv.symm (prodEquiv (M₁ := M₁)) :
        (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
          ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
      f =
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
Tactic: rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
rw :
  f = g ↔
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f) =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
rw₁ :
  f = g ↔
    (Equiv.symm (prodEquiv (M₁ := M₁)) :
          (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
            ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
        f =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
⊢ f = g ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g
have rw₂ : f = g ↔
  Eq (α := ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
    ((Equiv.symm (prodEquiv (M₁ := M₁)) :
          (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
            ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
        f :
      ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
    ((Equiv.symm (prodEquiv (M₁ := M₁)) :
          (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
            ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
        g :
      ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
Tactic: rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : (i : ι) → TopologicalSpace (M₁ i)
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
rw :
  f = g ↔
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f) =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
rw₁ :
  f = g ↔
    (Equiv.symm (prodEquiv (M₁ := M₁)) :
          (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
            ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
        f =
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g,
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g)
rw₂ :
  f = g ↔
    Eq (α := ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
      ((Equiv.symm (prodEquiv (M₁ := M₁)) :
            (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
              ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
          f :
        ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
      ((Equiv.symm (prodEquiv (M₁ := M₁)) :
            (a : ContinuousMultilinearMap R M₁ (M₂ × M₃)) →
              ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
          g :
        ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃)
⊢ f = g ↔
    ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.fst R M₂ M₃) g ∧
      ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) f =
        ContinuousLinearMap.compContinuousMultilinearMap (M₁ := M₁) (ContinuousLinearMap.snd R M₂ M₃) g
have rw₃ : f = g ↔ f = g
Tactic: rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
inst_8 : DecidableEq ι
inst_9 : Fintype ι
x y : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
have unfold : Eq.{w₂ + 1} (α := M₂)
  ((∑ i : ι,
          ContinuousLinearMap.comp (σ₂₃ := RingHom.id R)
            (let __src := f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x i;
            { toLinearMap := __src, cont := sorry })
            (ContinuousLinearMap.proj (φ := M₁) i) :
        (a : (i : ι) → M₁ i) → M₂)
      y :
    M₂)
  (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
Tactic: unfold linearDeriv toContinuousLinearMap