awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
s : Set M
z : M
f g : M → E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
hs : UniqueMDiffWithinAt I s z
⊢ mfderivWithin I 𝓘(𝕜, E') (f - g) s z =
    HSub.hSub (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z)))
      (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z)))
      (mfderivWithin I 𝓘(𝕜, E') f s z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (f z)))
      (mfderivWithin I 𝓘(𝕜, E') g s z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (g z)))

Tactic:
(hf.hasMFDerivWithinAt.sub hg.hasMFDerivWithinAt).mfderivWithin hs

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.sub, HasMFDerivWithinAt.mfderivWithin, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
F : Type u_11
inst_16 : NormedAddCommGroup F
inst_17 : NormedSpace 𝕜 F
G : Type u_12
inst_18 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_19 : TopologicalSpace N
inst_20 : ChartedSpace G N
F' : Type u_14
inst_21 : NormedAddCommGroup F'
inst_22 : NormedSpace 𝕜 F'
G' : Type u_15
inst_23 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_24 : TopologicalSpace N'
inst_25 : ChartedSpace G' N'
F₁ : Type u_17
inst_26 : NormedAddCommGroup F₁
inst_27 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_28 : NormedAddCommGroup F₂
inst_29 : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst_30 : NormedAddCommGroup F₃
inst_31 : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst_32 : NormedAddCommGroup F₄
inst_33 : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z))

Tactic:
exact mfderiv% f z

Premises used: mfderiv, modelWithCornersSelf
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
F : Type u_11
inst_16 : NormedAddCommGroup F
inst_17 : NormedSpace 𝕜 F
G : Type u_12
inst_18 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_19 : TopologicalSpace N
inst_20 : ChartedSpace G N
F' : Type u_14
inst_21 : NormedAddCommGroup F'
inst_22 : NormedSpace 𝕜 F'
G' : Type u_15
inst_23 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_24 : TopologicalSpace N'
inst_25 : ChartedSpace G' N'
F₁ : Type u_17
inst_26 : NormedAddCommGroup F₁
inst_27 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_28 : NormedAddCommGroup F₂
inst_29 : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst_30 : NormedAddCommGroup F₃
inst_31 : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst_32 : NormedAddCommGroup F₄
inst_33 : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z))

Tactic:
exact mfderiv% g z

Premises used: mfderiv, modelWithCornersSelf
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
z : M
f g : M → E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ mfderiv% (f - g) z =
    HSub.hSub (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z)))
      (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f - g) z)))
      (mfderiv% f z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (f z)))
      (mfderiv% g z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (g z)))

Tactic:
(hf.hasMFDerivAt.sub hg.hasMFDerivAt).mfderiv

Premises used: HasMFDerivAt.mfderiv, MDifferentiableAt.hasMFDerivAt, instModuleTangentSpace._aux_1, HasMFDerivAt.sub, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 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'
⊢ HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, F') z (p * q)) (p z •> q' + p' <• q z)
    ((↑(extChartAt I z).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I z) : M → E) z)

Tactic:
simpa only [mfld_simps] using hp.2.mul' hq.2

Premises used: And.right, HasFDerivWithinAt.mul'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
z : M
F' : Type u_21
inst_6 : NormedRing 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 : HasMFDerivAt I 𝓘(𝕜, F') p z p'
hq : HasMFDerivAt I 𝓘(𝕜, F') q z q'
⊢ HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z •> q' + p' <• q z)

Tactic:
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.mul' hq.hasMFDerivWithinAt

Premises used: HasMFDerivWithinAt.mul', hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, Iff.mp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 q : M → F'
hp : MDiffAt[s] p z
hq : MDiffAt[s] q z
⊢ MDiffAt[s] (p * q) z

Tactic:
(hp.hasMFDerivWithinAt.mul' hq.hasMFDerivWithinAt).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.mul'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
z : M
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiffAt p z
hq : MDiffAt q z
⊢ MDiffAt (p * q) z

Tactic:
(hp.hasMFDerivAt.mul' hq.hasMFDerivAt).mdifferentiableAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt, HasMFDerivAt.mul'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiff[s] p
hq : MDiff[s] q
⊢ MDiff[s] (p * q)

Tactic:
fun x hx ↦ (hp x hx).mul <| hq x hx

Premises used: MDifferentiableWithinAt.mul, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiff p
hq : MDiff q
⊢ MDiff (p * q)

Tactic:
fun x ↦ (hp x).mul (hq x)

Premises used: MDifferentiableAt.mul, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
⊢ MDiffAt[s] (HPow.hPow (β := ℕ) p 0) z

Tactic:
simpa [pow_zero] using mdifferentiableWithinAt_const

Premises used: mdifferentiableWithinAt_const, pow_zero
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : ℕ
hn : MDiffAt[s] (p ^ n) z
⊢ MDiffAt[s] (p ^ (n + 1)) z

Tactic:
simpa [pow_succ] using hn.mul hp

Premises used: MDifferentiableWithinAt.mul, pow_succ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
succ : ∀ (n : ℕ) (hn : MDiffAt[s] (p ^ n) z), MDiffAt[s] (p ^ (n + 1)) z
⊢ MDiffAt[s] (p ^ n) z

Tactic:
induction n with
  | zero => simpa [pow_zero] using mdifferentiableWithinAt_const
  | succ n hn => simpa [pow_succ] using hn.mul hp

Premises used: pow_succ, mdifferentiableWithinAt_const, pow_zero
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
z : M
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt p z
n : ℕ
⊢ MDiffAt (p ^ n) z

Tactic:
mdifferentiableWithinAt_univ.mp (hp.mdifferentiableWithinAt.pow n)

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableWithinAt_univ, Iff.mp, MDifferentiableWithinAt.pow
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiff[s] p
n : ℕ
⊢ MDiff[s] (p ^ n)

Tactic:
fun x hx ↦ (hp x hx).pow n

Premises used: MDifferentiableOn, MDifferentiableWithinAt.pow
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
F' : Type u_21
inst_6 : NormedRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiff p
n : ℕ
⊢ MDiff (p ^ n)

Tactic:
fun x ↦ (hp x).pow n

Premises used: MDifferentiableAt.pow, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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' + MulOpposite.op (q z) • p')

Tactic:
hp.mul' hq

Premises used: HasMFDerivWithinAt.mul'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
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)))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p')

Tactic:
convert! hp.mul' hq

Premises used: HasMFDerivWithinAt.mul'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
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')
⊢ 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:
ext _
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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'
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:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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
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 : HasMFDerivAt I 𝓘(𝕜, F') p z p'
hq : HasMFDerivAt I 𝓘(𝕜, F') q z q'
⊢ HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z • q' + q z • p')

Tactic:
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.mul hq.hasMFDerivWithinAt

Premises used: hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, Iff.mp, HasMFDerivWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : ι), 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:
simpa using hasMFDerivWithinAt_const ..

Premises used: hasMFDerivWithinAt_const
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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.insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)
insert :
  HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (Insert.insert i t).erase x, f j z) (f' x) +
      HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ Insert.insert i t, f i) s z
    (∑ i_1 ∈ Insert.insert i t, HSMul.hSMul (α := F') (∏ j ∈ (Insert.insert i t).erase i_1, f j z) (f' i_1))

Tactic:
rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]

Premises used: Finset.prod_insert, add_comm, Finset.erase_insert, Finset.sum_insert
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)

Tactic:
rw [t.forall_mem_insert] at hf

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 * ∏ i ∈ t, f i) s z
    (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)) +
      HSMul.hSMul (α := F') ((∏ i ∈ t, f i) z) (f' i))

Tactic:
hf.1.mul (IH hf.2)

Premises used: And.right, And.left, HasMFDerivWithinAt.mul