awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
f : M → E'
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderiv% (-f) x) (-mfderiv% f x)
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
  (mfderivWithin I 𝓘(𝕜, E') (-f) univ x) (-mfderiv% f x)
Tactic: rw [← mfderivWithin_univ, mfderivWithin_neg _ _ (uniqueMDiffWithinAt_univ I), mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
f : M → E'
x : M
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderivWithin I 𝓘(𝕜, E') (-f) univ x) (-mfderiv% f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderiv% (-f) x) (-mfderiv% f x)
have rw₁ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
  (-mfderivWithin I 𝓘(𝕜, E') f univ x :
    ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') (f x)))
  (-mfderiv% f x)
Tactic: rw [← mfderivWithin_univ, mfderivWithin_neg _ _ (uniqueMDiffWithinAt_univ I), mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
f : M → E'
x : M
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderivWithin I 𝓘(𝕜, E') (-f) univ x) (-mfderiv% f x)
rw₁ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (-mfderivWithin I 𝓘(𝕜, E') f univ x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (-mfderiv% f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderiv% (-f) x) (-mfderiv% f x)
have rw₂ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
  (-mfderiv% f x :
    ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') (f x)))
  (-mfderiv% f x)
Tactic: rw [← mfderivWithin_univ, mfderivWithin_neg _ _ (uniqueMDiffWithinAt_univ I), mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt[s] p z
n : ℕ
⊢ MDiffAt[s] (p ^ n) z
have zero : MDiffAt[s] (HPow.hPow (β := ℕ) p 0) z
Tactic: induction n with
  | zero => simpa [pow_zero] using mdifferentiableWithinAt_const
  | succ n hn => simpa [pow_succ] using hn.mul hp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt[s] p z
n : ℕ
zero : MDiffAt[s] (HPow.hPow (β := ℕ) p 0) z
⊢ MDiffAt[s] (p ^ n) z
have succ : ∀ (n : ℕ) (hn : MDiffAt[s] (p ^ n) z), MDiffAt[s] (p ^ (n + 1)) z
Tactic: induction n with
  | zero => simpa [pow_zero] using mdifferentiableWithinAt_const
  | succ n hn => simpa [pow_succ] using hn.mul hp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p')
have h : Eq (α :=
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F')
  (HSMul.hSMul (q z)) (HSMul.hSMul (MulOpposite.op (q z)))
Tactic: convert! hp.mul' hq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
      ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F')
    (HSMul.hSMul (q z)) (HSMul.hSMul (MulOpposite.op (q z)))
have h : ∀ (x : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (x_1 : TangentSpace I z),
  Eq.{u_21 + 1} (α := F') ((q z • x : (a : TangentSpace I z) → F') x_1 : F')
    ((MulOpposite.op (q z) • x : (a : TangentSpace I z) → F') x_1 : F')
Tactic: ext _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : ∀ i_1 ∈ insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ insert i t, f i) s z
    (∑ i_1 ∈ insert i t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase i_1, f j z) (f' i_1))
have insert : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
  (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) +
    HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))
Tactic: rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : ∀ i_1 ∈ insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) +
      HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))
have hf₁ : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
Tactic: rw [t.forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) +
      HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))
have h : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
  ∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (f i z)
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
Tactic: convert! hf.1.mul (IH hf.2) using 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
h :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
        (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
      ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
    ∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) =
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (f i z)
        (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) +
      HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))
have h₁ : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
  HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i) = HSMul.hSMul (α := F') ((∏ i ∈ t, f i) z) (f' i)
Tactic: convert! hf.1.mul (IH hf.2) using 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
⊢ ∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (f i z)
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
have h : Eq (α :=
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
    (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)))
  (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x))
  (∑ x ∈ t, (f i z * ∏ j ∈ t.erase x, f j z) • f' x)
Tactic: simp only [t.smul_sum, ← mul_smul]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)))
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x))
    (∑ x ∈ t, (f i z * ∏ j ∈ t.erase x, f j z) • f' x)
have h : ∀ (j : ι) (hj : j ∈ t),
  HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase j, f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
Tactic: refine t.sum_congr rfl (fun j hj ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
j : ι
hj : j ∈ t
⊢ HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase j, f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
have h : HSMul.hSMul (α := F') (∏ j ∈ insert i (t.erase j), f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
Tactic: rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
j : ι
hj : j ∈ t
h : HSMul.hSMul (α := F') (∏ j ∈ insert i (t.erase j), f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
⊢ HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase j, f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
have h₁ : (f i z * ∏ x ∈ t.erase j, f x z) • f' j = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
Tactic: rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
  HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ ∅, f i) s z
    (∑ i ∈ ∅, HSMul.hSMul (α := F') (∏ j ∈ Finset.erase ∅ i, f j z) (f' i))
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i t hi IH =>
    rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]
    rw [t.forall_mem_insert] at hf
    convert! hf.1.mul (IH hf.2) using 2
    · simp only [t.smul_sum, ← mul_smul]
      refine t.sum_congr rfl (fun j hj ↦ ?_)
      rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
    · simp
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ ∅, f i) s z
      (∑ i ∈ ∅, HSMul.hSMul (α := F') (∏ j ∈ Finset.erase ∅ i, f j z) (f' i))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
      HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
        (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i)))
  (hf : ∀ i_1 ∈ insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)),
  HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ insert i t, f i) s z
    (∑ i_1 ∈ insert i t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase i_1, f j z) (f' i_1))
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i t hi IH =>
    rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]
    rw [t.forall_mem_insert] at hf
    convert! hf.1.mul (IH hf.2) using 2
    · simp only [t.smul_sum, ← mul_smul]
      refine t.sum_congr rfl (fun j hj ↦ ?_)
      rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
    · simp
Cleared hypotheses: hf