awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
inst_7 : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a : ℝ | ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun (x : ℝ) ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun (x : ℝ) ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t : ℝ | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t : ℝ | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M :=
  (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
γ_ext_def :
  γ_ext =
    (Ioo (-(asup + ε / 2)) a).piecewise (β := fun (a : ℝ) ↦ M) ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ IsMIntegralCurveOn ((Ioo (-a) a).piecewise (β := fun (i : ℝ) ↦ M) γ γ1) v (Ioo (-(asup + ε / 2)) a)

Tactic:
exact (isMIntegralCurveOn_piecewise (t₀ := -(asup - ε / 2)) hv hγ hγ1
      ⟨⟨neg_lt_neg hlt, by linarith⟩, ⟨by linarith, by linarith⟩⟩ heq1.symm).mono
    (union_comm _ _ ▸ Ioo_subset_Ioo_union_Ioo (by linarith) (by linarith) le_rfl)

Premises used: IsMIntegralCurveOn.mono, isMIntegralCurveOn_piecewise, neg_lt_neg, And.intro, Eq.symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
e : PartialEquiv α β
he : Continuous[inst_1, inst] (↑e.symm : β → α)
⊢ Continuous[inst_1, inst] e.invFun

Tactic:
he
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
rw : range (↑I.toPartialEquiv : H → E) = (↑I.toPartialEquiv : H → E) '' I.source
rw₁ : range (↑I.toPartialEquiv : H → E) = (↑I.toPartialEquiv : H → E) '' univ
rw₂ rw₃ : (↑I.toPartialEquiv : H → E) '' univ = (↑I.toPartialEquiv : H → E) '' univ
⊢ range (↑I.toPartialEquiv : H → E) = I.target

Tactic:
rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]

Premises used: Set.image_univ, ModelWithCorners.toPartialEquiv, ModelWithCorners.source_eq, PartialEquiv.image_source_eq_target, Eq.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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
rw : range (↑φ : H → E) = (↑φ : H → E) '' φ.source
rw₁ : range (↑φ : H → E) = (↑φ : H → E) '' univ
rw₂ rw₃ : (↑φ : H → E) '' univ = (↑φ : H → E) '' univ
⊢ range (↑φ : H → E) = φ.target

Tactic:
rw [← φ.image_source_eq_target, hsource, image_univ.symm]

Premises used: Set.image_univ, PartialEquiv.image_source_eq_target, Eq.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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
⊢ range (↑φ : H → E) = φ.target

Tactic:
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
this : range (↑φ : H → E) = φ.target
simp : ∀ (h : IsRCLikeNormedField 𝕜), Convex.{0, u_2} ℝ (E := E) univ
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ

Tactic:
simp only [this, htarget, dite_else_true]

Premises used: dite_else_true
-- 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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
this_1 : range (↑φ : H → E) = φ.target
h : IsRCLikeNormedField 𝕜
this_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex.{0, u_2} ℝ (E := E) univ

Tactic:
convex_univ

Premises used: 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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
this_1 : range (↑φ : H → E) = φ.target
h : IsRCLikeNormedField 𝕜
this_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex.{0, u_2} ℝ (E := E) univ

Tactic:
exact convex_univ

Premises used: 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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑φ.symm : E → H)
this : range (↑φ : H → E) = φ.target
⊢ (interior (range (↑φ : H → E))).Nonempty

Tactic:
simp [this, htarget]
-- 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.toPartialEquiv : H → E) = (↑I : H → E)

Tactic:
rfl

Premises used: ModelWithCorners.toFun', 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
e : PartialEquiv H E
a : e.source = univ
b : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑e : H → E)) else range (↑e : H → E) = univ
c : (interior (range (↑e : H → E))).Nonempty
d : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e : H → E)
d' : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] e.invFun
⊢ (↑{ toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d,
          continuous_invFun := d' : ModelWithCorners 𝕜 E H } :
      H → E) =
    (↑e : H → E)

Tactic:
rfl

Premises used: ModelWithCorners.toFun', 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
⊢ (↑I.symm : E → H) = (↑I.symm : E → H)

Tactic:
rfl

Premises used: 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
e : PartialEquiv H E
a : e.source = univ
b : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑e : H → E)) else range (↑e : H → E) = univ
c : (interior (range (↑e : H → E))).Nonempty
d : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑e : H → E)
d' : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] e.invFun
⊢ { toPartialEquiv := e, source_eq := a, convex_range' := b, nonempty_interior' := c, continuous_toFun := d,
        continuous_invFun := d' : ModelWithCorners 𝕜 E H }.symm =
    e.symm

Tactic:
rfl

Premises used: ModelWithCorners.symm, 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
⊢ Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I : H → E)

Tactic:
I.continuous_toFun

Premises used: ModelWithCorners.toFun', ModelWithCorners.continuous_toFun
-- 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
⊢ ContinuousAt (↑I : H → E) x

Tactic:
I.continuous.continuousAt

Premises used: Continuous.continuousAt, ModelWithCorners.continuous
-- 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
⊢ ContinuousWithinAt (↑I : H → E) s x

Tactic:
I.continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, ModelWithCorners.continuousAt
-- 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
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_3] (↑I.symm : E → H)

Tactic:
I.continuous_invFun

Premises used: ModelWithCorners.continuous_invFun
-- 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
⊢ ContinuousAt (↑I.symm : E → H) x

Tactic:
I.continuous_symm.continuousAt

Premises used: Continuous.continuousAt, ModelWithCorners.continuous_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
s : Set E
x : E
⊢ ContinuousWithinAt (↑I.symm : E → H) s x

Tactic:
I.continuous_symm.continuousWithinAt

Premises used: ModelWithCorners.continuous_symm, Continuous.continuousWithinAt
-- 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 E
⊢ ContinuousOn (↑I.symm : E → H) s

Tactic:
I.continuous_symm.continuousOn

Premises used: Continuous.continuousOn, ModelWithCorners.continuous_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
rw : I.target = (↑I : H → E) '' I.source
⊢ I.target = range (↑I : H → E)

Tactic:
rw [← image_univ, ← I.source_eq]

Premises used: Set.image_univ, 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
⊢ I.target = (↑I : H → E) '' I.source

Tactic:
I.image_source_eq_target.symm

Premises used: ModelWithCorners.toPartialEquiv, PartialEquiv.image_source_eq_target, ModelWithCorners.toFun', Eq.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
⊢ I.target = (↑I : H → E) '' I.source

Tactic:
exact I.image_source_eq_target.symm

Premises used: ModelWithCorners.toPartialEquiv, PartialEquiv.image_source_eq_target, Eq.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
⊢ (interior (range (↑I : H → E))).Nonempty

Tactic:
I.nonempty_interior'

Premises used: ModelWithCorners.toFun', 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) = univ

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
inst_3 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
hv : v ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • u + b • v ∈ s

Tactic:
hs 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
inst_3 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
hv : v ∈ s
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 ∈ s

Tactic:
convert! hs 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
inst_3 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
hv : v ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u = a • u
h₂ h₃ :
  HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u =
    HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u
⊢ a • u = a • u

Tactic:
rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @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
inst_3 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
u : E
hu : u ∈ s
v : E
hv : v ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v = b • v
h₂ h₃ :
  HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v =
    HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v
⊢ b • v = b • v

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

Premises used: algebraMap_smul
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
rw : range (↑φ : H → E) = (↑φ : H → E) '' φ.source
rw₁ : range (↑φ : H → E) = (↑φ : H → E) '' univ
rw₂ rw₃ : (↑φ : H → E) '' univ = (↑φ : H → E) '' univ
⊢ range (↑φ : H → E) = φ.target

Tactic:
rw [← φ.image_source_eq_target, hsource, image_univ.symm]

Premises used: Set.image_univ, PartialEquiv.image_source_eq_target, Eq.symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
⊢ range (↑φ : H → E) = φ.target

Tactic:
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
this : range (↑φ : H → E) = φ.target
simp : Convex ℝ φ.target
⊢ if h : IsRCLikeNormedField ℝ then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ

Tactic:
simp only [instIsRCLikeNormedField, ↓reduceDIte, this]

Premises used: reduceDIte, instIsRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
this : range (↑φ : H → E) = φ.target
⊢ Convex ℝ φ.target

Tactic:
htarget.convex_isRCLikeNormedField

Premises used: Convex.convex_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
this : range (↑φ : H → E) = φ.target
⊢ Convex ℝ φ.target

Tactic:
exact htarget.convex_isRCLikeNormedField

Premises used: Convex.convex_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E_1 H_1
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
H : Type u_5
inst_6 : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑φ : H → E)
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_6] (↑φ.symm : E → H)
hint : (interior φ.target).Nonempty
this : range (↑φ : H → E) = φ.target
⊢ (interior (range (↑φ : H → E))).Nonempty

Tactic:
simp [this, hint]
-- 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
pos : ∀ (h : IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E))
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E))
⊢ Convex ℝ (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
inst_4 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I.toPartialEquiv : H → E))
  else range (↑I.toPartialEquiv : H → E) = univ

Tactic:
have W := I.convex_range'