awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_4 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W :
  ∀ ⦃x : E⦄,
    x ∈ range (↑I : H → E) →
      ∀ ⦃y : E⦄, y ∈ range (↑I : H → E) → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range (↑I : H → E)
u : E
hu : u ∈ range (↑I : H → E)
v : E
hv : v ∈ range (↑I : H → E)
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • u = a • u
have h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u = a • u
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_4 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W :
  ∀ ⦃x : E⦄,
    x ∈ range (↑I : H → E) →
      ∀ ⦃y : E⦄, y ∈ range (↑I : H → E) → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range (↑I : H → E)
u : E
hu : u ∈ range (↑I : H → E)
v : E
hv : v ∈ range (↑I : H → E)
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b • v = b • v
have h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v = b • v
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))
have pos : ∀ (h : IsRCLikeNormedField 𝕜), UniqueDiffOn 𝕜 (range (↑I : H → E))
Tactic: by_cases h : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
pos : ∀ (h : IsRCLikeNormedField 𝕜), UniqueDiffOn 𝕜 (range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), UniqueDiffOn 𝕜 (range (↑I : H → E))
Tactic: by_cases h : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))
have apply : Convex ℝ (range (↑I : H → E))
Tactic: apply uniqueDiffOn_convex_of_isRCLikeNormedField _ I.nonempty_interior
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
have pos : ∀ (h : IsRCLikeNormedField 𝕜),
  range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
Tactic: by_cases h : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
pos :
  ∀ (h : IsRCLikeNormedField 𝕜),
    range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜),
  range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
Tactic: by_cases h : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
have pos : range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range (↑I : H → E))
Tactic: rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
pos : range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range (↑I : H → E))
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
have pos₁ : Convex ℝ (range (↑I : H → E))
Tactic: rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
pos : range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range (↑I : H → E))
pos₁ : Convex ℝ (range (↑I : H → E))
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
have pos₂ : (interior (range (↑I : H → E))).Nonempty
Tactic: rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
⊢ (↑I.symm : E → H) ((↑I : H → E) x) = x
have refine : x ∈ I.source
Tactic: refine I.left_inv' ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
⊢ (↑I : H → E) '' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
have refine_1 : s ⊆ I.source
Tactic: refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
refine_1 : s ⊆ I.source
⊢ (↑I : H → E) '' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
have refine_2 : I.target ∩ (↑I.symm : E → H) ⁻¹' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
Tactic: refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
⊢ s ⊆ I.source
have refine_1 : s ⊆ univ
Tactic: rw [I.source_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
⊢ I.target ∩ (↑I.symm : E → H) ⁻¹' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
have refine_2 : (↑I.symm : E → H) ⁻¹' s ∩ I.target = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
Tactic: rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
refine_2 : (↑I.symm : E → H) ⁻¹' s ∩ I.target = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ I.target ∩ (↑I.symm : E → H) ⁻¹' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
have refine_2₁ : (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
Tactic: rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
refine_2 : (↑I.symm : E → H) ⁻¹' s ∩ I.target = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
refine_2₁ : (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ I.target ∩ (↑I.symm : E → H) ⁻¹' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
have refine_2₂ : (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
Tactic: rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
s : Set H
⊢ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' s] (↑I : H → E) x) = 𝓝[s] x
have rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝[s] x)) = 𝓝[s] x
Tactic: rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
s : Set H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝[s] x)) = 𝓝[s] x
⊢ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' s] (↑I : H → E) x) = 𝓝[s] x
have rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝[s] x) = 𝓝[s] x
Tactic: rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
s : Set H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝[s] x)) = 𝓝[s] x
rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝[s] x) = 𝓝[s] x
⊢ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' s] (↑I : H → E) x) = 𝓝[s] x
have rw₂ : map id (𝓝[s] x) = 𝓝[s] x
Tactic: rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
s : Set H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝[s] x)) = 𝓝[s] x
rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝[s] x) = 𝓝[s] x
rw₂ : map id (𝓝[s] x) = 𝓝[s] x
⊢ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' s] (↑I : H → E) x) = 𝓝[s] x
have rw₃ : 𝓝[s] x = 𝓝[s] x
Tactic: rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
⊢ map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x) = 𝓝 x
have rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝 x)) = 𝓝 x
Tactic: rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝 x)) = 𝓝 x
⊢ map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x) = 𝓝 x
have rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝 x) = 𝓝 x
Tactic: rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝 x)) = 𝓝 x
rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝 x) = 𝓝 x
⊢ map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x) = 𝓝 x
have rw₂ : map id (𝓝 x) = 𝓝 x
Tactic: rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
x : H
rw : map (↑I.symm : E → H) (map (↑I : H → E) (𝓝 x)) = 𝓝 x
rw₁ : map ((↑I.symm : E → H) ∘ (↑I : H → E)) (𝓝 x) = 𝓝 x
rw₂ : map id (𝓝 x) = 𝓝 x
⊢ map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x) = 𝓝 x
have rw₃ : 𝓝 x = 𝓝 x
Tactic: rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
hs : IsOpen[inst_3] s
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
have rw : UniqueDiffOn 𝕜 (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' s)
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x) ↔
    ContinuousWithinAt f s x
have refine_1 : ∀ (h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)),
  ContinuousWithinAt f s x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
refine_1 :
  ∀ (h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)),
    ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x) ↔
    ContinuousWithinAt f s x
have refine_2 : ∀ (h : ContinuousWithinAt f s x),
  ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContinuousWithinAt f s x
have this : ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E))
  ((↑I : H → E) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))) x
Tactic: have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E))
    ((↑I : H → E) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))) x
⊢ ContinuousWithinAt f s x
have this₁ : ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E)) s x
Tactic: simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
      inter_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
this : ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E)) s x
⊢ ContinuousWithinAt f s x
have refine_1 : ∀ (this : ContinuousWithinAt (f ∘ (↑I.symm : E → H) ∘ (↑I : H → E)) s x), ContinuousWithinAt f s x
Tactic: rwa [Function.comp_assoc, I.symm_comp_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
this : ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E)) s x
refine_1 : ∀ (this : ContinuousWithinAt (f ∘ (↑I.symm : E → H) ∘ (↑I : H → E)) s x), ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x
have refine_1₁ : ∀ (this : ContinuousWithinAt (f ∘ id) s x), ContinuousWithinAt f s x
Tactic: rwa [Function.comp_assoc, I.symm_comp_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
have h₁ : ContinuousWithinAt f s ((↑I.symm : E → H) ((↑I : H → E) x))
Tactic: rw [← I.left_inv x] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
have rw : (map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x)).HasBasis
  (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
  (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
Tactic: rw [← I.symm_map_nhdsWithin_range]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
⊢ LocallyCompactSpace H
have this : ∀ (x : H),
  (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
Tactic: have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x) ∧ IsCompact s)
      fun s => I.symm '' (s ∩ range I) := fun x ↦ by
    rw [← I.symm_map_nhdsWithin_range]
    exact ((compact_basis_nhds (I x)).inf_principal _).map _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
⊢ LocallyCompactSpace H
have refine : ∀ (x : H) (i : Set E), i ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact i → IsCompact ((↑I.symm : E → H) '' (i ∩ range (↑I : H → E)))
Tactic: refine .of_hasBasis this ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.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
inst_5 : ChartedSpace H M
⊢ T1Space M
have this : T2Space H
Tactic: have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type w'
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (E := E × E') (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2))
  else Eq (α := Set (E × E')) (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have this : (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) =
  range (Prod.map (↑I : H → E) (↑I' : H' → E'))
Tactic: have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl