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
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: classical
  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: classical
  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
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, HasMFDerivAt I 𝓘(𝕜, F') (f i) z (f' i)
⊢ HasMFDerivAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) z (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
have simp_all : ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) univ z (f' i)),
  HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) univ z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
Tactic: simp_all only [← hasMFDerivWithinAt_univ]
Cleared hypotheses: hf
-- 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
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt (f i) z
⊢ MDiffAt (∏ i ∈ t, f i) z
have hf₁ : ∀ i ∈ t, MDiffAt[univ] (f i) z
Tactic: simp_all only [← mdifferentiableWithinAt_univ]
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 : 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 (-(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p')
have h : -(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' = -(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p')
Tactic: convert! hp.inv' hp_ne
-- 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 : 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
⊢ -(HPow.hPow (β := ℕ) (p z) 2)⁻¹ • p' = -(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p')
have 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')
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 : 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
⊢ 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')
have 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)⁻¹
Tactic: simp
-- 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 : 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 ((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q')
have h : p / q = p * q⁻¹
Tactic: convert! hp.mul (hq.inv hq_ne) using 1
-- 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 : 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⁻¹
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p / q) s z ((1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q')
have 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'
Tactic: convert! hp.mul (hq.inv hq_ne) using 1
-- 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 : 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⁻¹
⊢ (1 / q z) • p' - (p z / HPow.hPow (β := ℕ) (q z) 2) • q' = p z • -(HPow.hPow (β := ℕ) (q z) 2)⁻¹ • q' + q⁻¹ z • p'
have 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')
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 : 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
⊢ 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')
have 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')
Tactic: simp [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
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)),
      (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))
have 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))
Tactic: rw [MDifferentiableAt.mfderiv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
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))
⊢ 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))
have rw₁ : MDiffAt (↑(chartAt H (p.proj (E := TangentSpace I))) : M → H) (q.proj (E := TangentSpace I))
Tactic: rw [MDifferentiableAt.mfderiv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
inst_6 : IsManifold I 1 M
p : TangentBundle I M
q : TangentBundle I H
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).target
⊢ ⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
      (mfderiv% (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M)
            (q.proj (E := TangentSpace I)) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
        (q.snd (E := TangentSpace I))⟩ =
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p) :
            OpenPartialHomeomorph (ModelProd H E) (TangentBundle I M)) :
        ModelProd H E → TangentBundle I M)
      ((TotalSpace.toProd H E : (a : TotalSpace E fun (x : H) ↦ E) → H × E) q : H × E)
have rw : ⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
    (fderivWithin 𝕜
          (writtenInExtChartAt I I (q.proj (E := TangentSpace I))
            (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M))
          (range (↑I : H → E))
          ((↑(extChartAt I (q.proj (E := TangentSpace I))) : H → E) (q.proj (E := TangentSpace I))) :
        (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
      (q.snd (E := TangentSpace I))⟩ =
  (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p) :
          OpenPartialHomeomorph (ModelProd H E) (TangentBundle I M)) :
      ModelProd H E → TangentBundle I M)
    ((TotalSpace.toProd H E : (a : TotalSpace E fun (x : H) ↦ E) → H × E) q : H × E)
Tactic: rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
inst_6 : IsManifold I 1 M
x y : M
hsrc : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H y)).source
⊢ mfderiv% (↑(chartAt H y) : M → H) x = tangentCoordChange I x y x
have this : MDiffAt (↑(ChartedSpace.chartAt y) : M → H) x
Tactic: have := mdifferentiableAt_atlas (I := I) (ChartedSpace.chart_mem_atlas _) hsrc
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ inTangentCoordinates I I' f g ϕ x₀ x =
    mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
      ϕ x ∘SL
        mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I (f x₀)) : M → E) (f x))
have rw : Eq (α := E →L[𝕜] E')
  (fderivWithin 𝕜
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
          (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
        (range (↑I' : H' → E'))
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) ∘SL
      ϕ x ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M)
          (achart H (f x₀)) (achart H (f x)) (f x) :
    E →L[𝕜] E')
  (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
      ϕ x ∘SL
        mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I (f x₀)) : M → E) (f x)) :
    ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜)
      (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
      (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x))))
Tactic: rw [inTangentCoordinates_eq _ _ _ hx hy, tangentBundleCore_coordChange]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ Eq (α := E →L[𝕜] E')
    (fderivWithin 𝕜
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
            (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
          (range (↑I' : H' → E'))
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) ∘SL
        ϕ x ∘SL
          VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M)
            (achart H (f x₀)) (achart H (f x)) (f x) :
      E →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
        ϕ x ∘SL
          mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I (f x₀)) : M → E) (f x)) :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜)
        (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
        (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x))))
have e_g : Eq (α := E' →L[𝕜] E')
  (fderivWithin 𝕜
      ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
        (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
      (range (↑I' : H' → E'))
      ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) :
    E' →L[𝕜] E')
  (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) :
    TangentSpace I' (g x) →L[𝕜] TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x)))
Tactic: congr