awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
mp :
  ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x →
    ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)
⊢ ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x ↔
    ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)
have mpr : ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x) →
  ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
Hfh : ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x
⊢ ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)
have Hfh₁ : ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s ((h.symm : (a : N) → M) ((h : (a : M) → N) x : N))
Tactic: rw [← h.symm_apply_apply x] at Hfh
Cleared hypotheses: Hfh
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x) →
    ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x
have mpr : ContMDiffWithinAt J I' m f ((⇑h : (a : M) → N) '' s) ((h : (a : M) → N) x) →
  ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x
Tactic: rw [← h.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_11
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
hn : n ≠ 0
s : Set M
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn.{u_1, u_4, u_7, u_11} J (M := N) ((⇑h : (a : M) → N) '' s)
have h₁ : (⇑h : (a : M) → N) '' s =
  h.toHomeomorph.toOpenPartialHomeomorph.target ∩ (↑h.toHomeomorph.toOpenPartialHomeomorph.symm : N → M) ⁻¹' s
Tactic: convert! hs.uniqueMDiffOn_preimage (h.toOpenPartialHomeomorph_mdifferentiable hn)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
  else range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ
have pos : ∀ (h : IsRCLikeNormedField 𝕜),
  Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
pos :
  ∀ (h : IsRCLikeNormedField 𝕜),
    Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
  else range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E') = univ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))
have pos : Convex.{0, u_3} ℝ (E := E') (range ((⇑e : (a : E) → E') ∘ (↑I : H → E)))
Tactic: simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
h : IsRCLikeNormedField 𝕜
⊢ Convex.{0, u_3} ℝ (E := E') (range ((⇑e : (a : E) → E') ∘ (↑I : H → E)))
have pos : Convex.{0, u_3} ℝ (E := E') ((⇑e : (a : E) → E') '' range (↑I : H → E))
Tactic: rw [range_comp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
eR : E →L[ℝ] E' := ContinuousLinearMap.restrictScalars ℝ (↑e : E →L[𝕜] E')
⊢ Convex.{0, u_3} ℝ (E := E') ((⇑e : (a : E) → E') '' range (↑I : H → E))
have pos : Convex.{0, u_3} ℝ (E := E') ((⇑eR : (a : E) → E') '' range (↑I : H → E))
Tactic: change Convex ℝ (⇑eR '' range ↑I)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (interior (range (↑(I.toPartialEquiv ≫ (↑e : E ≃ₗ[𝕜] E').toEquiv.toPartialEquiv) : H → E'))).Nonempty
have simp : Set.Nonempty.{u_3} (α := E') (interior ((⇑e.symm : (a : E') → E) ⁻¹' range (↑I : H → E)))
Tactic: simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe, range_comp,
      ContinuousLinearEquiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ Set.Nonempty.{u_3} (α := E') (interior ((⇑e.symm : (a : E') → E) ⁻¹' range (↑I : H → E)))
have apply : Set.Nonempty.{u_3} (α := E') ((⇑e.symm : (a : E') → E) ⁻¹' interior (range (↑I : H → E)))
Tactic: apply Nonempty.mono (preimage_interior_subset_interior_preimage e.symm.continuous)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ Set.Nonempty.{u_3} (α := E') ((⇑e.symm : (a : E') → E) ⁻¹' interior (range (↑I : H → E)))
have rw : Set.Nonempty.{u_3} (α := E') ((⇑e : (a : E) → E') '' interior (range (↑I : H → E)))
Tactic: rw [← ContinuousLinearEquiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] F
inst_19 : IsManifold I n M
⊢ IsManifold (I.transContinuousLinearEquiv e) n M
have refine : ∀ (e₁ e₂ : OpenPartialHomeomorph M H) (h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁)
  (h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂),
  ContDiffOn 𝕜 n
    ((↑(I.transContinuousLinearEquiv e) : H → F) ∘
      (↑(e₁.symm ≫ₕ e₂) : H → H) ∘ (↑(I.transContinuousLinearEquiv e).symm : F → H))
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))
Tactic: refine isManifold_of_contDiffOn (I.transContinuousLinearEquiv e) n M fun e₁ e₂ h₁ h₂ => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] F
inst_19 : IsManifold I n M
e₁ e₂ : OpenPartialHomeomorph M H
h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₁
h₂ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e₂
⊢ ContDiffOn 𝕜 n
    ((↑(I.transContinuousLinearEquiv e) : H → F) ∘
      (↑(e₁.symm ≫ₕ e₂) : H → H) ∘ (↑(I.transContinuousLinearEquiv e).symm : F → H))
    ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
      range (↑(I.transContinuousLinearEquiv e) : H → F))
have refine : MapsTo (↑((↑e : E ≃ₗ[𝕜] F).toEquiv.toPartialEquiv.restr I.target).symm : F → E)
  ((↑(I.transContinuousLinearEquiv e).symm : F → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩
    range (↑(I.transContinuousLinearEquiv e) : H → F))
  ((↑I.symm : E → H) ⁻¹' (e₁.symm ≫ₕ e₂).source ∩ range (↑I : H → E))
Tactic: refine e.contDiff.comp_contDiffOn
      (((contDiffGroupoid n I).compatible h₁ h₂).1.comp e.symm.contDiff.contDiffOn ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
⊢ ContMDiffAt I (I.transContinuousLinearEquiv e) (M' := M) n (⇑(Equiv.refl M) : (a : M) → M) x
have refine : ContDiffWithinAt 𝕜 n
  (comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
    ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M))
  ((extChartAt I x).target ∩
    (↑(extChartAt I x).symm : E → M) ⁻¹'
      (univ ∩
        preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
          (PartialEquiv.source.{u_9, u_4} (β := F)
              (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
            Set M)))
  ((↑(extChartAt I x) : M → E) x)
Tactic: refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M))
    ((extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M)))
    ((↑(extChartAt I x) : M → E) x)
have refine_1 : ∀ (y : E)
  (hy :
    y ∈
      (extChartAt I x).target ∩
        (↑(extChartAt I x).symm : E → M) ⁻¹'
          (univ ∩
            preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
              (PartialEquiv.source.{u_9, u_4} (β := F)
                  (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
                Set M))),
  comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M) y =
    (e : (a : E) → F) y
Tactic: refine e.contDiff.contDiffWithinAt.congr_of_mem (fun y hy ↦ ?_) ?_