awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
⊢ (↑I : H → E) (e ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ((↑I.symm : E → H) z))) = z
have right : (↑I : H → E) ((↑I.symm : E → H) z) = z
Tactic: rw [h.toOpenPartialHomeomorph_right_inv e this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst_5 : Nonempty M
this_1 : IsManifold I ω M
z_1 : H
hz_1 : M
z : E
hz :
  z ∈
    (extChartAt I z_1).target ∩
      (↑(extChartAt I z_1).symm : E → H) ⁻¹'
        (range e ∩ (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm : H → M) ⁻¹' (extChartAt I hz_1).source)
this : (↑I.symm : E → H) z ∈ range e
⊢ (↑I : H → E) ((↑I.symm : E → H) z) = z
have right : z ∈ range (↑I : H → E)
Tactic: apply I.right_inv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
⊢ f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
have h : ∀ (x : M), f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
x : M
⊢ f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x
have h : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ((e' ∘ f) x)
Tactic: rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
x : M
h : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ((e' ∘ f) x)
⊢ f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x
have h₁ : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') (e' (f x))
Tactic: rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
x : M
h : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ((e' ∘ f) x)
h₁ : f x = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') (e' (f x))
⊢ f x = ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f) x
have h₂ : f x = f x
Tactic: rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
⊢ ContMDiff I I' n f
have this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
Tactic: have : f = (h'.toOpenPartialHomeomorph e').symm ∘ e' ∘ f := by
    ext
    rw [Function.comp_apply, Function.comp_apply, IsOpenEmbedding.toOpenPartialHomeomorph_left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
⊢ ContMDiff I I' n f
have rw : ContMDiff I I' n ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
n : ℕ∞ω
inst_9 : ChartedSpace H M
inst_10 : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
this : f = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f
⊢ ContMDiff I I' n ((↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm : H' → M') ∘ e' ∘ f)
have apply : ∀ (x : M), (e' ∘ f) x ∈ range e'
Tactic: apply @ContMDiffOn.comp_contMDiff _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
    h'.singletonChartedSpace _ _ (range e') _ (contMDiffOn_isOpenEmbedding_symm h') hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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'
s : Set M
x : M
n : WithTop ℕ∞
f : M → M'
g : M → N'
hf : ContMDiffWithinAt I I' n f s x
hg : ContMDiffWithinAt I J' n g s x
⊢ ContMDiffWithinAt I (I'.prod J') (M' := M' × N') n (fun (x : M) ↦ (f x, g x)) s x
have rw : ∀
  (hf :
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (hg :
    ContinuousWithinAt g s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt J' (g x)) : N' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)),
  ContinuousWithinAt (Y := M' × N') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt (I'.prod J') (f x, g x)) : M' × N' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [contMDiffWithinAt_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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'
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x
hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x
⊢ ContMDiffWithinAt I (E' := E' × F') 𝓘(𝕜, E' × F') (M' := E' × F') n (fun (x : M) ↦ (f x, g x)) s x
have rw : ∀
  (hf :
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, E') (f x)) : E' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (hg :
    ContinuousWithinAt g s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt 𝓘(𝕜, F') (g x)) : F' → F') ∘ g ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)),
  ContinuousWithinAt (Y := E' × F') (fun (x : M) ↦ (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 (F := E' × F') n
      ((↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) : E' × F' → E' × F') ∘
        (fun (x : M) ↦ (f x, g x)) ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [contMDiffWithinAt_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContMDiffWithinAt (I.prod J) I n Prod.fst s p
have rw : ContinuousWithinAt Prod.fst s p ∧
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
    ((extChartAt (I.prod J) p).target ∩
      (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source))
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
Tactic: rw [contMDiffWithinAt_iff']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContinuousWithinAt Prod.fst s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
have refine_1 : ∀ (y : E × F)
  (hy :
    y ∈
      (extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source)),
  ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.1
Tactic: refine ⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
refine_1 :
  ∀ (y : E × F)
    (hy :
      y ∈
        (extChartAt (I.prod J) p).target ∩
          (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source)),
    ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.1
⊢ ContinuousWithinAt Prod.fst s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.fst ⁻¹' (extChartAt I p.1).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
have refine_2 : ((↑(extChartAt I p.1) : M → E) ∘ Prod.fst ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
  ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).1
Tactic: refine ⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContMDiffWithinAt (I.prod J) J n Prod.snd s p
have rw : ContinuousWithinAt Prod.snd s p ∧
  ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
    ((extChartAt (I.prod J) p).target ∩
      (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source))
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
Tactic: rw [contMDiffWithinAt_iff']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ ContinuousWithinAt Prod.snd s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
have refine_1 : ∀ (y : E × F)
  (hy :
    y ∈
      (extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)),
  ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.2
Tactic: refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_9
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
refine_1 :
  ∀ (y : E × F)
    (hy :
      y ∈
        (extChartAt (I.prod J) p).target ∩
          (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)),
    ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N)) y = y.2
⊢ ContinuousWithinAt Prod.snd s p ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
      ((extChartAt (I.prod J) p).target ∩
        (↑(extChartAt (I.prod J) p).symm : E × F → M × N) ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source))
      ((↑(extChartAt (I.prod J) p) : M × N → E × F) p)
have refine_2 : ((↑(extChartAt J p.2) : N → F) ∘ Prod.snd ∘ (↑(extChartAt (I.prod J) p).symm : E × F → M × N))
    ((↑(extChartAt (I.prod J) p) : M × N → E × F) p) =
  ((↑(extChartAt (I.prod J) p) : M × N → E × F) p).2
Tactic: refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x
have rw : ContMDiffWithinAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s x ↔
  ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x
have rw : ContMDiffAt I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f x ↔
  ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
s : Set M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffOn I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f s ↔
    ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s
have rw : ContMDiffOn I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f s ↔
  ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (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_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (E' := F₁ × F₂) 𝓘(𝕜, F₁ × F₂) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)
have rw : ContMDiff I (ModelWithCorners.prod 𝓘(𝕜, F₁) 𝓘(𝕜, F₂)) n f ↔
  ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)
Tactic: rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]