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'
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'
s : Set (M × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
⊢ Eq (α := TangentBundle I M)
    ⟨p.proj (E := TangentSpace (I.prod I')).1,
      ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
            Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
                (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
              TangentSpace I p.proj (E := TangentSpace (I.prod I')).1) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩
have rcases : ∀ (proj : M × M') (snd : TangentSpace (I.prod I') proj)
  (hs : UniqueMDiffWithinAt (I.prod I') s (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)),
  Eq (α := TangentBundle I M)
    ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1,
      ((ContinuousLinearMap.fst 𝕜
              (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
              (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) :
            Prod.{u_2, u_5}
                (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
                (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) →L[𝕜]
              TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1) :
          (a : TangentSpace (I.prod I') ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj.1)
        (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)⟩
    ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1,
      (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1⟩
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p, hs
-- 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'
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'
x : M × M'
⊢ HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
have refine : HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I' x Prod.snd)
  (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
  (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
Tactic: refine ⟨continuous_snd.continuousAt, ?_⟩
-- 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'
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'
x : M × M'
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
have h : ∀ (y : E × E') (hy : y ∈ (extChartAt (I.prod I') x).target),
  ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
Tactic: filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
-- 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
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'
x : M × M'
y : E × E'
hy : y ∈ (extChartAt (I.prod I') x).target
⊢ ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
have hy₁ : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
Tactic: rw [extChartAt_prod] at hy
Cleared hypotheses: hy
-- 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
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'
x : M × M'
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I' x Prod.snd)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
have this : ∀ᶠ (y : E × E') in 𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
  ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
Tactic: have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I' x.2 ∘ Prod.snd ∘ (extChartAt (I.prod I') x).symm) y = y.2 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I' x.2).right_inv hy.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
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'
x : M × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I' x Prod.snd)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
have apply : ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
  ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).2
Tactic: apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_snd this
-- 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'
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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderivWithin (I.prod I') I' Prod.snd s x)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
have rw : Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderiv% Prod.snd x)
  (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
Tactic: rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]
-- 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
F₁ : Type u_17
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x
have rw : MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- 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
F₁ : Type u_17
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x
have rw : MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- 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
F₁ : Type u_17
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
f : M → F₁ × F₂
⊢ MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)
have rw : MDiff[s] f ↔ MDiff[s] (Prod.fst ∘ f) ∧ MDiff[s] (Prod.snd ∘ f)
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- 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
F₁ : Type u_17
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)
have rw : MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- 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
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt f x
hg : MDiffAt g y
⊢ MDiffAt (Prod.map f g) (x, y)
have hf₁ : MDiffAt[univ] f x
Tactic: rw [← mdifferentiableWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- 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
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt f x
hg : MDiffAt g y
hf₁ : MDiffAt[univ] f x
⊢ MDiffAt (Prod.map f g) (x, y)
have hg₁ : MDiffAt[univ] g y
Tactic: rw [← mdifferentiableWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- 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'
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ MDiffAt[univ] (Prod.map f g) (x, y)
have h : univ = SProd.sprod (α := Set M) (β := Set N) univ univ
Tactic: convert! hf.prodMap hg
-- 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'
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivWithinAt I J f (Prod.fst '' s) p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivWithinAt I' J' g (Prod.snd '' s) p.2 dg
⊢ HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) s p (df.prodMap dg)
have refine : HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') (J.prod J') p (Prod.map f g)) (df.prodMap dg)
  ((↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E'))
  ((↑(extChartAt (I.prod I') p) : M × M' → E × E') p)
Tactic: refine ⟨hf.1.prodMap hg.1 |>.mono (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
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivWithinAt I J f (Prod.fst '' s) p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivWithinAt I' J' g (Prod.snd '' s) p.2 dg
⊢ (↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E') ⊆
    ((↑(extChartAt I p.1).symm : E → M) ⁻¹' Prod.fst '' s ∩ range (↑I : H → E)) ×ˢ
      ((↑(extChartAt I' p.2).symm : E' → M') ⁻¹' Prod.snd '' s ∩ range (↑I' : H' → E'))
have simp : (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).prod
                (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2))).symm :
          ModelProd H H' → M × M') ∘
        (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') ⁻¹'
      s ∩
    range (Prod.map (↑I : H → E) (↑I' : H' → E')) ⊆
  ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' s ∩
      range (↑I : H → E)) ×ˢ
    ((↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s ∩
      range (↑I' : H' → E'))
Tactic: simp only [mfld_simps]
-- 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'
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'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivWithinAt I J f (Prod.fst '' s) p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivWithinAt I' J' g (Prod.snd '' s) p.2 dg
⊢ (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).prod
                  (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2))).symm :
            ModelProd H H' → M × M') ∘
          (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') ⁻¹'
        s ∩
      range (Prod.map (↑I : H → E) (↑I' : H' → E')) ⊆
    ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' s ∩
        range (↑I : H → E)) ×ˢ
      ((↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s ∩
        range (↑I' : H' → E'))
have rw : (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).symm.prod
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2)).symm) :
          ModelProd H H' → M × M') ∘
        (↑(I.symm.prod I'.symm) : E × E' → ModelProd H H') ⁻¹'
      s ∩
    range (↑I : H → E) ×ˢ range (↑I' : H' → E') ⊆
  ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' s ∩
      range (↑I : H → E)) ×ˢ
    ((↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s ∩
      range (↑I' : H' → E'))
Tactic: rw [range_prodMap, I.toPartialEquiv.prod_symm, (chartAt H p.1).toPartialEquiv.prod_symm]