awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E)) ((↑I : H → E) ((↑(ChartedSpace.chartAt x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((v, 0) : E × E)
have B₁ : Eq (α := E × E)
  (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          E →L[𝕜] E × E) :
        (a : E) → E × E)
      v :
    E × E)
  ((v, 0) : TangentSpace I x × E)
Tactic: rw [← fderivWithin_inter N] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E)) ((↑I : H → E) ((↑(ChartedSpace.chartAt x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((v, 0) : E × E)
have rw : Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
  ((fderivWithin 𝕜
          (fun (x_1 : E) ↦
            ((↑I : H → E)
                ((↑(ChartedSpace.chartAt x) : M → H)
                  ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
              0))
          (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
          ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
        (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
      v :
    TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
  (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          E →L[𝕜] E × E) :
        (a : E) → E × E)
      v :
    E × E)
Tactic: rw [← fderivWithin_inter N, ← B]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
have e_a : Eq (α :=
  TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
  (fderivWithin 𝕜
    (fun (x_1 : E) ↦
      ((↑I : H → E)
          ((↑(ChartedSpace.chartAt x) : M → H)
            ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
        0))
    (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
  (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
    (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α :=
    TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (fderivWithin 𝕜
      (fun (x_1 : E) ↦
        ((↑I : H → E)
            ((↑(ChartedSpace.chartAt x) : M → H)
              ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
          0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
have e_a : ∀ (y : E)
  (hy : y ∈ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target),
  Eq (α := E × E)
    ((↑I : H → E)
        ((↑(ChartedSpace.chartAt x) : M → H)
          ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) y))),
      0)
    (y, 0)
Tactic: refine fderivWithin_congr (fun y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
e_a :
  ∀ (y : E)
    (hy : y ∈ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target),
    Eq (α := E × E)
      ((↑I : H → E)
          ((↑(ChartedSpace.chartAt x) : M → H)
            ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) y))),
        0)
      (y, 0)
⊢ Eq (α :=
    TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (fderivWithin 𝕜
      (fun (x_1 : E) ↦
        ((↑I : H → E)
            ((↑(ChartedSpace.chartAt x) : M → H)
              ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
          0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
have e_a₁ : Eq (α := E × E)
  ((↑I : H → E)
      ((↑(ChartedSpace.chartAt x) : M → H)
        ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M)
          ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))))),
    0)
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x), 0)
Tactic: refine fderivWithin_congr (fun y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
y : E
hy : y ∈ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ Eq (α := E × E)
    ((↑I : H → E)
        ((↑(ChartedSpace.chartAt x) : M → H)
          ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) y))),
      0)
    (y, 0)
have hy₁ : y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (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'
⊢ Eq (α := (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)
have simp : Eq (α := (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
  (⇑(equivTangentBundleProd I M I' M') :
    (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
  fun (p : TangentBundle (I.prod I') (M × M')) ↦
  (⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩,
    ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩)
Tactic: simp only [tangentMap_prodFst, tangentMap_prodSnd]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
⊢ ContMDiff (I.prod I').tangent (M := TangentBundle (I.prod I') (M × M')) (I.tangent.prod I'.tangent) (M' :=
    TangentBundle I M × TangentBundle I' M') n
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
have rw : ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) (M' := TangentBundle I M × TangentBundle I' M') n
  fun (p : TangentBundle (I.prod I') (M × M')) ↦
  (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)
Tactic: rw [equivTangentBundleProd_eq_tangentMap_prod_tangentMap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
have simp : UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
Tactic: simp only [range_prodMap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
have hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) w)
Tactic: apply UniqueDiffWithinAt.prod
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) w)
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
have ht : UniqueDiffWithinAt 𝕜 (range (↑I' : H' → E')) ((↑I' : H' → E') w')
Tactic: apply UniqueDiffWithinAt.prod
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I').tangent (M' := TangentBundle (I.prod I') (M × M')) n
    (⇑(Equiv.symm (equivTangentBundleProd I M I' M')) :
      (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
    (a, b)
have U : ∀ (w : H) (w' : H'),
  UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
Tactic: have U w w' : UniqueDiffWithinAt 𝕜 (Set.range (Prod.map I I')) (I w, I' w') := by
    simp only [range_prodMap]
    apply UniqueDiffWithinAt.prod
    · exact ModelWithCorners.uniqueDiffWithinAt_image I
    · exact ModelWithCorners.uniqueDiffWithinAt_image I'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I').tangent (M' := TangentBundle (I.prod I') (M × M')) n
    (⇑(Equiv.symm (equivTangentBundleProd I M I' M')) :
      (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
    (a, b)
have rw : ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
    (fun (x : TangentBundle I M × TangentBundle I' M') ↦
      TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I'))
        ((Equiv.symm (equivTangentBundleProd I M I' M') :
            (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
          x))
    (a, b) ∧
  ContMDiffAt (I.tangent.prod I'.tangent) (E' := E × E') 𝓘(𝕜, E × E') (M' := E × E') n
    (fun (x : TangentBundle I M × TangentBundle I' M') ↦
      ((↑(trivializationAt (E × E') (TangentSpace (I.prod I'))
                (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I'))
                  ((Equiv.symm (equivTangentBundleProd I M I' M') :
                      (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
                    (a, b)))) :
            TotalSpace (E × E') (TangentSpace (I.prod I')) → (M × M') × E × E')
          ((Equiv.symm (equivTangentBundleProd I M I' M') :
              (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
            x)).2)
    (a, b)
Tactic: rw [contMDiffAt_totalSpace]