awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 :
  if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I.toPartialEquiv : H → E))
  else range (↑I.toPartialEquiv : H → E) = univ
⊢ Convex ℝ (range (↑I : H → E))

Tactic:
simp only [h, ↓reduceDIte, toPartialEquiv_coe] at W

Premises used: reduceDIte, ModelWithCorners.toPartialEquiv_coe
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 + b • v ∈ range (↑I : H → E)

Tactic:
W hu hv ha hb hab
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
h₁ : a • u = a • u
h₂ : b • v = b • v
⊢ a • u + b • v ∈ range (↑I : H → E)

Tactic:
convert! W hu hv ha hb hab using 2
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u = a • u
⊢ a • u = a • u

Tactic:
rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]

Premises used: algebraMap_smul
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u = a • u

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v = b • v
⊢ b • v = b • v

Tactic:
rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]

Premises used: algebraMap_smul
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v = b • v

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 𝕜
⊢ Convex ℝ (range (↑I : H → E))

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField I h, convex_univ]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField, convex_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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))
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), UniqueDiffOn 𝕜 (range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Premises used: IsRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
apply : Convex ℝ (range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))

Tactic:
apply uniqueDiffOn_convex_of_isRCLikeNormedField _ I.nonempty_interior

Premises used: ModelWithCorners.nonempty_interior, uniqueDiffOn_convex_of_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ Convex ℝ (range (↑I : H → E))

Tactic:
simpa [h] using I.convex_range

Premises used: ModelWithCorners.convex_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 𝕜
⊢ UniqueDiffOn 𝕜 (range (↑I : H → E))

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField I h, uniqueDiffOn_univ]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField, uniqueDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)))
neg :
  ∀ (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)))

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Premises used: IsRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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))
pos₂ : (interior (range (↑I : H → E))).Nonempty
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))

Tactic:
rw [Convex.closure_interior_eq_closure_of_nonempty_interior (𝕜 := ℝ)]

Premises used: Convex.closure_interior_eq_closure_of_nonempty_interior
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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] (range (↑I : H → E))

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ Convex ℝ (range (↑I : H → E))

Tactic:
apply I.convex_range

Premises used: ModelWithCorners.convex_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ (interior (range (↑I : H → E))).Nonempty

Tactic:
apply I.nonempty_interior

Premises used: ModelWithCorners.nonempty_interior
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 𝕜
⊢ range (↑I : H → E) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField I h]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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

Tactic:
I.left_inv' ?_

Premises used: ModelWithCorners.toPartialEquiv, ModelWithCorners.toFun', PartialEquiv.left_inv'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
refine : x ∈ I.source
⊢ (↑I.symm : E → H) ((↑I : H → E) x) = x

Tactic:
refine I.left_inv' ?_

Premises used: ModelWithCorners.toPartialEquiv, PartialEquiv.left_inv'
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ x ∈ I.source

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ LeftInverse (↑I.symm : E → H) (↑I : H → E)

Tactic:
I.left_inv

Premises used: Function.LeftInverse, ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ Injective (↑I : H → E)

Tactic:
I.leftInverse.injective

Premises used: Function.LeftInverse.injective, ModelWithCorners.leftInverse
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ (↑I.symm : E → H) ∘ (↑I : H → E) = id

Tactic:
I.leftInverse.comp_eq_id

Premises used: ModelWithCorners.leftInverse, Function.LeftInverse.comp_eq_id
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ RightInvOn (↑I.symm : E → H) (↑I : H → E) (range (↑I : H → E))

Tactic:
I.leftInverse.rightInvOn_range

Premises used: ModelWithCorners.leftInverse, Function.LeftInverse.rightInvOn_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : E
hx : x ∈ range (↑I : H → E)
⊢ (↑I : H → E) ((↑I.symm : E → H) x) = x

Tactic:
I.rightInvOn hx

Premises used: ModelWithCorners.rightInvOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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) ⁻¹' (↑I : H → E) '' s = s

Tactic:
I.injective.preimage_image s

Premises used: ModelWithCorners.injective, Function.Injective.preimage_image
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)

Tactic:
(I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_

Premises used: ModelWithCorners.toPartialEquiv, PartialEquiv.image_eq_target_inter_inv_preimage, ModelWithCorners.toFun', Eq.trans
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
refine_2 : I.target ∩ (↑I.symm : E → H) ⁻¹' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑I : H → E) '' s = (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_

Premises used: ModelWithCorners.toPartialEquiv, PartialEquiv.image_eq_target_inter_inv_preimage, Eq.trans
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 ⊆ univ
⊢ s ⊆ I.source

Tactic:
rw [I.source_eq]

Premises used: ModelWithCorners.source_eq
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 ⊆ univ

Tactic:
subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 ⊆ univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)
refine_2₂ 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)

Tactic:
rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]

Premises used: Set.inter_comm, ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ IsClosedEmbedding (↑I : H → E)

Tactic:
I.leftInverse.isClosedEmbedding I.continuous_symm I.continuous

Premises used: ModelWithCorners.leftInverse, ModelWithCorners.continuous, ModelWithCorners.continuous_symm, Function.LeftInverse.isClosedEmbedding
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range (↑I : H → E))

Tactic:
I.isClosedEmbedding.isClosed_range

Premises used: ModelWithCorners.isClosedEmbedding, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)))

Tactic:
Subset.antisymm I.range_subset_closure_interior I.isClosed_range.closure_interior_subset

Premises used: Set.Subset.antisymm, ModelWithCorners.range_subset_closure_interior, IsClosed.closure_interior_subset, ModelWithCorners.isClosed_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : H → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) x

Tactic:
I.isClosedEmbedding.isEmbedding.map_nhds_eq x

Premises used: Topology.IsClosedEmbedding.isEmbedding, ModelWithCorners.isClosedEmbedding, Topology.IsEmbedding.map_nhds_eq
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
x : H
⊢ map (↑I : H → E) (𝓝[s] x) = 𝓝[(↑I : H → E) '' s] (↑I : H → E) x

Tactic:
I.isClosedEmbedding.isEmbedding.map_nhdsWithin_eq s x

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.map_nhdsWithin_eq, ModelWithCorners.isClosedEmbedding
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
hs : s ∈ 𝓝 x
⊢ (↑I : H → E) '' s ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x

Tactic:
I.map_nhds_eq x ▸ image_mem_map hs

Premises used: Eq.rec, Filter.image_mem_map, ModelWithCorners.map_nhds_eq
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
rw₃ rw₄ : 𝓝[s] x = 𝓝[s] x
⊢ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' s] (↑I : H → E) x) = 𝓝[s] x

Tactic:
rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]

Premises used: ModelWithCorners.symm_comp_self, ModelWithCorners.map_nhdsWithin_eq, Filter.map_map, Filter.map_id
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
rw₃ rw₄ : 𝓝 x = 𝓝 x
⊢ map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x) = 𝓝 x

Tactic:
rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]

Premises used: ModelWithCorners.symm_comp_self, Filter.map_map, ModelWithCorners.map_nhds_eq, Filter.map_id
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
rw : UniqueDiffOn 𝕜 (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' s)
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 𝕜 (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' s)

Tactic:
I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

Premises used: ModelWithCorners.continuous_invFun, UniqueDiffOn.inter, IsOpen.preimage, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 𝕜 (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' s)

Tactic:
exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

Premises used: ModelWithCorners.continuous_invFun, UniqueDiffOn.inter, IsOpen.preimage, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
β : Type u_4
inst_4 : TopologicalSpace β
e : OpenPartialHomeomorph H β
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' e.source ∩ range (↑I : H → E))

Tactic:
I.uniqueDiffOn_preimage e.open_source

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.uniqueDiffOn_preimage