awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
have this : let this := borel F;
BorelSpace F
Tactic: borelize F
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
have inl : ∀ (hα : SecondCountableTopology α), StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
Tactic: rcases h.out with hα | hF
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
inl : ∀ (hα : SecondCountableTopology α), StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
have inr : ∀ (hF : SecondCountableTopology F), StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
Tactic: rcases h.out with hα | hF
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
hα : SecondCountableTopology α
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
have this : ProperSpace 𝕜
Tactic: have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
⊢ StronglyMeasurable (β := F) fun (p : α × 𝕜) ↦ deriv (f p.1) p.2
have apply : IsSeparable.{u_3} (α := F) (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
Tactic: apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_deriv_with_param hf, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
have rw : deriv (f p.1) p.2 ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f p.1 '' univ)) : Set F)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) p ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)
have A : deriv (f p.1) p.2 ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
Tactic: have A : deriv (f p.1) p.2 ∈ closure (Submodule.span 𝕜 (range (f p.1))) := by
        rw [← image_univ]
        apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A :
  deriv (f p.1) p.2 ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (range (f p.1))) : Set F)
⊢ (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) p ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)
have B : range (f p.1) ⊆ range (Function.uncurry f)
Tactic: have B : range (f p.1) ⊆ range (f.uncurry) := by
        rintro - ⟨x, rfl⟩
        exact mem_range_self (p.1, x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
α : Type u_4
inst_3 : TopologicalSpace α
inst_4 : MeasurableSpace α
inst_5 : OpensMeasurableSpace α
inst_6 : CompleteSpace F
inst_7 : LocallyCompactSpace 𝕜
inst_8 : MeasurableSpace 𝕜
inst_9 : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this_1 : MeasurableSpace F := borel F
this_2 : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
⊢ IsSeparable.{u_3} (α := F) (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
have this₁ : (range fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (↑(Submodule.span 𝕜 (range (Function.uncurry f))) : Set F)
Tactic: have : range (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)
        ⊆ closure (Submodule.span 𝕜 (range f.uncurry)) := by
      rintro - ⟨p, rfl⟩
      have A : deriv (f p.1) p.2 ∈ closure (Submodule.span 𝕜 (range (f p.1))) := by
        rw [← image_univ]
        apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)
      have B : range (f p.1) ⊆ range (f.uncurry) := by
        rintro - ⟨x, rfl⟩
        exact mem_range_self (p.1, x)
      exact closure_mono (Submodule.span_mono B) A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (c * d) (c x •> d' + d x •> c') x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
Tactic: convert! hc.mul' hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
have h : ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
  Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (c * d) (c x •> d' + d x •> c') s x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
Tactic: convert! hc.mul' hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
have h : ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
  Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (c * d) (c x •> d' + d x •> c') x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
Tactic: convert! hc.mul' hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
have h : ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
  Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HasStrictFDerivAt (fun (y : E) ↦ c y * d) (d •> c') x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
Tactic: convert! hc.mul_const' d
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
have h : ∀ (z : E →L[𝕜] 𝔸') (x : E), Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x : 𝔸') ((z <• d : (a : E) → 𝔸') x : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y * d) (d •> c') s x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
Tactic: convert! hc.mul_const' d
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
have h : ∀ (z : E →L[𝕜] 𝔸') (x : E), Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x : 𝔸') ((z <• d : (a : E) → 𝔸') x : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HasFDerivAt (fun (y : E) ↦ c y * d) (d •> c') x
have h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
Tactic: convert! hc.mul_const' d
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
have h : ∀ (z : E →L[𝕜] 𝔸') (x : E), Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x : 𝔸') ((z <• d : (a : E) → 𝔸') x : 𝔸')
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
l : List ι
x : ι → 𝔸
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
have have : ∀ (this : Fintype ι),
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i sorry) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x (a :: l)).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
    x
have cons : HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸)
  (fun (x : ι → 𝔸) ↦
    HMul.hMul (α := 𝔸) ((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) (List.map x l).prod)
  (∑ i : Fin (a :: l).length,
    (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸)
          (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i sorry) <•
        (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
  x
Tactic: simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
⊢ ((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) •>
        ∑ i : Fin l.length,
          (List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸)
                (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
              (List.map x (List.drop (↑i : ℕ).succ l)).prod) +
      proj (φ := fun (x : ι) ↦ 𝔸) a <• (List.map x l).prod =
    ∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod)
have h : ∀ (x_1 : ι → 𝔸),
  Eq.{u_6 + 1} (α := 𝔸)
    ((((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) •>
              ∑ i : Fin l.length,
                (List.map x (List.take (↑i : ℕ) l)).prod •>
                  (proj (φ := fun (a : ι) ↦ 𝔸)
                      (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i sorry) <•
                    (List.map x (List.drop (↑i : ℕ).succ l)).prod) +
            proj (φ := fun (x : ι) ↦ 𝔸) a <• (List.map x l).prod :
          (a : ι → 𝔸) → 𝔸)
        x_1 :
      𝔸)
    ((∑ i : Fin (a :: l).length,
            (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
              (proj (φ := fun (a : ι) ↦ 𝔸)
                  (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i
                    sorry) <•
                (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod) :
          (a : ι → 𝔸) → 𝔸)
        x_1 :
      𝔸)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
l : List ι
x : ι → 𝔸
this : Fintype ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
have nil : HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x []).prod)
  (∑ i : Fin [].length,
    (List.map x (List.take (↑i : ℕ) [])).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸)
          (getElem (valid := fun (xs : List ι) (i : Fin (List.length.{u_5} (α := ι) [])) ↦ (↑i : ℕ) < xs.length) [] i
            sorry) <•
        (List.map x (List.drop (↑i : ℕ).succ [])).prod))
  x
Tactic: induction l with
  | nil => simp [hasStrictFDerivAt_const]
  | cons a l IH =>
    simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
    exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
l : List ι
x : ι → 𝔸
this : Fintype ι
nil :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x []).prod)
    (∑ i : Fin [].length,
      (List.map x (List.take (↑i : ℕ) [])).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (List.length.{u_5} (α := ι) [])) ↦ (↑i : ℕ) < xs.length) [] i
              ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ [])).prod))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
have cons : ∀ (a : ι) (l : List ι)
  (IH :
    HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
      (∑ i : Fin l.length,
        (List.map x (List.take (↑i : ℕ) l)).prod •>
          (proj (φ := fun (a : ι) ↦ 𝔸)
              (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i sorry) <•
            (List.map x (List.drop (↑i : ℕ).succ l)).prod))
      x),
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x (a :: l)).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i sorry) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
    x
Tactic: induction l with
  | nil => simp [hasStrictFDerivAt_const]
  | cons a l IH =>
    simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
    exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])
Cleared hypotheses: l