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
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiff (f i)
⊢ MDiff (∏ i ∈ t, f i)

Tactic:
fun z ↦ .prod fun i hi ↦ hf i hi z

Premises used: MDifferentiableAt.prod, 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') p⁻¹ s z (-((p z)⁻¹ •> p' <• (p z)⁻¹))

Tactic:
(hasFDerivAt_inv' hp_ne).hasMFDerivAt.comp_hasMFDerivWithinAt (hf := hp)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.hasMFDerivAt, instModuleTangentSpace._aux_1, HasMFDerivAt.comp_hasMFDerivWithinAt, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, MulOpposite.unop, 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
z : M
F' : Type u_21
inst_6 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivAt I 𝓘(𝕜, F') p z p'
hp_ne : p z ≠ 0
⊢ HasMFDerivAt I 𝓘(𝕜, F') p⁻¹ z (-((p z)⁻¹ •> p' <• (p z)⁻¹))

Tactic:
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.inv' hp_ne

Premises used: hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, Iff.mp, HasMFDerivWithinAt.inv'
-- 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt[s] p z
hp_ne : p z ≠ 0
⊢ MDiffAt[s] p⁻¹ z

Tactic:
(hp.hasMFDerivWithinAt.inv' hp_ne).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.inv'
-- 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiffAt p z
hp_ne : p z ≠ 0
⊢ MDiffAt p⁻¹ z

Tactic:
mdifferentiableWithinAt_univ.mp <| hp.mdifferentiableWithinAt.inv hp_ne

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableWithinAt_univ, MDifferentiableWithinAt.inv, 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
F' : Type u_21
inst_6 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiff[s] p
hp_ne : ∀ z ∈ s, p z ≠ 0
⊢ MDiff[s] p⁻¹

Tactic:
fun x hx ↦ (hp x hx).inv (hp_ne x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.inv
-- 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
hp : MDiff p
hp_ne : ∀ (z : M), p z ≠ 0
⊢ MDiff p⁻¹

Tactic:
fun x ↦ (hp x).inv (hp_ne x)

Premises used: MDifferentiableAt.inv, 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiffAt[s] p z
hq : MDiffAt[s] q z
hq_ne : q z ≠ 0
⊢ MDiffAt[s] (p / q) z

Tactic:
simpa [div_eq_mul_inv] using hp.mul (hq.inv hq_ne)

Premises used: MDifferentiableWithinAt.mul, div_eq_mul_inv, MDifferentiableWithinAt.inv
-- 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiffAt p z
hq : MDiffAt q z
hq_ne : q z ≠ 0
⊢ MDiffAt (p / q) z

Tactic:
simpa [div_eq_mul_inv] using hp.mul (hq.inv hq_ne)

Premises used: MDifferentiableAt.mul, MDifferentiableAt.inv, div_eq_mul_inv
-- 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 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiff[s] p
hq : MDiff[s] q
hq_ne : ∀ z ∈ s, q z ≠ 0
⊢ MDiff[s] (p / q)

Tactic:
simpa [div_eq_mul_inv] using hp.mul (hq.inv hq_ne)

Premises used: div_eq_mul_inv, MDifferentiableOn.inv, MDifferentiableOn.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
F' : Type u_21
inst_6 : NormedDivisionRing F'
inst_7 : NormedAlgebra 𝕜 F'
p q : M → F'
hp : MDiff p
hq : MDiff q
hq_ne : ∀ (z : M), q z ≠ 0
⊢ MDiff (p / q)

Tactic:
simpa [div_eq_mul_inv] using hp.mul (hq.inv hq_ne)

Premises used: div_eq_mul_inv, MDifferentiable.inv, MDifferentiable.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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') p⁻¹ s z (-(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p'))

Tactic:
hp.inv' hp_ne

Premises used: HasMFDerivWithinAt.inv'
-- 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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
h : -(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' = -(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p')
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') p⁻¹ s z (-(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p')

Tactic:
convert! hp.inv' hp_ne

Premises used: HasMFDerivWithinAt.inv'
-- 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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
h :
  ∀ (x : TangentSpace I z),
    Eq.{u_21 + 1} (α := F') ((-(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' : (a : TangentSpace I z) → F') x : F')
      ((-(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p') : (a : TangentSpace I z) → F') x : F')
⊢ -(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' = -(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p')

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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
x : TangentSpace I z
h :
  HMul.hMul (β := F') (HPow.hPow (β := ℕ) (p z) 2)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') =
    HMul.hMul (β := F') (p z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') * (p z)⁻¹
⊢ Eq.{u_21 + 1} (α := F') ((-(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' : (a : TangentSpace I z) → F') x : F')
    ((-(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p') : (a : TangentSpace I z) → F') x : F')

Tactic:
simp
-- 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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hp_ne : p z ≠ 0
x : TangentSpace I z
⊢ HMul.hMul (β := F') (HPow.hPow (β := ℕ) (p z) 2)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') =
    HMul.hMul (β := F') (p z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') * (p z)⁻¹

Tactic:
ring_nf
-- 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 : NormedField F'
inst_7 : NormedAlgebra 𝕜 F'
p : M → F'
p' : ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
hp : HasMFDerivAt I 𝓘(𝕜, F') p z p'
hp_ne : p z ≠ 0
⊢ HasMFDerivAt I 𝓘(𝕜, F') p⁻¹ z (-(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p')

Tactic:
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.inv hp_ne

Premises used: HasMFDerivWithinAt.inv, 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 : NormedField 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'
hq_ne : q z ≠ 0
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q⁻¹) s z (p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p')

Tactic:
hp.mul (hq.inv hq_ne)

Premises used: HasMFDerivWithinAt.inv, 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 : NormedField 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'
hq_ne : q z ≠ 0
h : p / q = p * q⁻¹
h₁ :
  p / q = p * q⁻¹ →
    (1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q' = p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p / q) s z ((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q')

Tactic:
convert! hp.mul (hq.inv hq_ne) using 1

Premises used: HasMFDerivWithinAt.inv, 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 : NormedField 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'
hq_ne : q z ≠ 0
⊢ p / q = p * q⁻¹

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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 : NormedField 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'
hq_ne : q z ≠ 0
e_21 : p / q = p * q⁻¹
h :
  ∀ (x : TangentSpace I z),
    Eq.{u_21 + 1} (α := F')
      (((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q' : (a : TangentSpace I z) → F') x : F')
      ((p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p' : (a : TangentSpace I z) → F') x : F')
⊢ (1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q' = p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p'

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 : NormedField 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'
hq_ne : q z ≠ 0
e_21 : p / q = p * q⁻¹
x : TangentSpace I z
h :
  HMul.hMul (β := F') (q z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') -
      HMul.hMul (β := F') (p z * (HPow.hPow (β := ℕ) (q z) 2)⁻¹) ((q' : (a : TangentSpace I z) → F') x : F') =
    -(p z * HMul.hMul (β := F') (HPow.hPow (β := ℕ) (q z) 2)⁻¹ ((q' : (a : TangentSpace I z) → F') x : F')) +
      HMul.hMul (β := F') (q z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F')
⊢ Eq.{u_21 + 1} (α := F')
    (((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q' : (a : TangentSpace I z) → F') x : F')
    ((p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p' : (a : TangentSpace I z) → F') x : F')

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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 : NormedField 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'
hq_ne : q z ≠ 0
e_21 : p / q = p * q⁻¹
x : TangentSpace I z
⊢ HMul.hMul (β := F') (q z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F') -
      HMul.hMul (β := F') (p z * (HPow.hPow (β := ℕ) (q z) 2)⁻¹) ((q' : (a : TangentSpace I z) → F') x : F') =
    -(p z * HMul.hMul (β := F') (HPow.hPow (β := ℕ) (q z) 2)⁻¹ ((q' : (a : TangentSpace I z) → F') x : F')) +
      HMul.hMul (β := F') (q z)⁻¹ ((p' : (a : TangentSpace I z) → F') x : F')

Tactic:
ring
-- 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 : NormedField 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'
hq_ne : q z ≠ 0
⊢ HasMFDerivAt I 𝓘(𝕜, F') (p / q) z ((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q')

Tactic:
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.div hq.hasMFDerivWithinAt hq_ne

Premises used: hasMFDerivWithinAt_univ, HasMFDerivAt.hasMFDerivWithinAt, Iff.mp, HasMFDerivWithinAt.div
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
p q : TangentBundle I M
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).source
rw :
  Eq (α := TangentBundle I H)
    ⟨(↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I)),
      (fderivWithin 𝕜
            (writtenInExtChartAt I I (q.proj (E := TangentSpace I))
              (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H))
            (range (↑I : H → E))
            ((↑(extChartAt I (q.proj (E := TangentSpace I))) : M → E) (q.proj (E := TangentSpace I))) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj) : M → H) q.proj))
        (q.snd (E := TangentSpace I))⟩
    (((TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)
      ((↑(chartAt (ModelProd H E) p) : TangentBundle I M → ModelProd H E) q))
rw₁ : MDiffAt (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I))
⊢ Eq (α := TangentBundle I H)
    ⟨(↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I)),
      (mfderiv% (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I)) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj) : M → H) q.proj))
        (q.snd (E := TangentSpace I))⟩
    (((TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)
      ((↑(chartAt (ModelProd H E) p) : TangentBundle I M → ModelProd H E) q))

Tactic:
rw [MDifferentiableAt.mfderiv]

Premises used: MDifferentiableAt.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
p q : TangentBundle I M
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).source
⊢ Eq (α := TangentBundle I H)
    ⟨(↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I)),
      (fderivWithin 𝕜
            (writtenInExtChartAt I I (q.proj (E := TangentSpace I))
              (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H))
            (range (↑I : H → E))
            ((↑(extChartAt I (q.proj (E := TangentSpace I))) : M → E) (q.proj (E := TangentSpace I))) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj) : M → H) q.proj))
        (q.snd (E := TangentSpace I))⟩
    (((TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)
      ((↑(chartAt (ModelProd H E) p) : TangentBundle I M → ModelProd H E) q))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
p q : TangentBundle I M
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).source
⊢ MDiffAt (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I))

Tactic:
mdifferentiableAt_atlas (chart_mem_atlas _ _) h

Premises used: chart_mem_atlas, mdifferentiableAt_atlas
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
p q : TangentBundle I M
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).source
⊢ MDiffAt (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I))

Tactic:
exact mdifferentiableAt_atlas (chart_mem_atlas _ _) h

Premises used: chart_mem_atlas, mdifferentiableAt_atlas