awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
linarith : ε - (asup - ε / 2) ≤ -a → 2 / 2 = 1
linarith₁ : ε - (asup - ε / 2) ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -a < ε - (asup - ε / 2)
have linarith₂ : ε - (asup - ε / 2) ≤ -a → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
linarith : ε - (asup - ε / 2) ≤ -a → 2 / 2 = 1
linarith₁ : ε - (asup - ε / 2) ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε - (asup - ε / 2) ≤ -a → GT.gt (α := ℝ) 2 0
linarith₃ : ε - (asup - ε / 2) ≤ -a → 2 / 2 = 1
linarith₄ : ε - (asup - ε / 2) ≤ -a → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε - (asup - ε / 2) ≤ -a → GT.gt (α := ℝ) 2 0
⊢ -a < ε - (asup - ε / 2)
have linarith₆ : ε - (asup - ε / 2) ≤ -a → 2 * (0 - ε) + (2 * asup - 1 * ε - 2 * a) + (2 * ε - (2 * asup - 1 * ε) - -(2 * a)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ range (↑I.toPartialEquiv : H → E) = I.target
have rw : range (↑I.toPartialEquiv : H → E) = (↑I.toPartialEquiv : H → E) '' I.source
Tactic: rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ range (↑I.toPartialEquiv : H → E) = I.target
have rw₁ : range (↑I.toPartialEquiv : H → E) = (↑I.toPartialEquiv : H → E) '' univ
Tactic: rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ range (↑I.toPartialEquiv : H → E) = I.target
have rw₂ : (↑I.toPartialEquiv : H → E) '' univ = (↑I.toPartialEquiv : H → E) '' univ
Tactic: rw [← I.image_source_eq_target, I.source_eq, image_univ.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
φ : 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
have rw : range (↑φ : H → E) = (↑φ : H → E) '' φ.source
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.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
φ : 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
⊢ range (↑φ : H → E) = φ.target
have rw₁ : range (↑φ : H → E) = (↑φ : H → E) '' univ
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.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
φ : 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
⊢ range (↑φ : H → E) = φ.target
have rw₂ : (↑φ : H → E) '' univ = (↑φ : H → E) '' univ
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- 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
φ : 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)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ
have this : range (↑φ : H → E) = φ.target
Tactic: have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.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
φ : 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
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ
have simp : ∀ (h : IsRCLikeNormedField 𝕜), Convex.{0, u_2} ℝ (E := E) univ
Tactic: simp only [this, htarget, dite_else_true]
-- 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
φ : 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)
⊢ (interior (range (↑φ : H → E))).Nonempty
have this : range (↑φ : H → E) = φ.target
Tactic: have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.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
⊢ I.target = range (↑I : H → E)
have rw : I.target = (↑I : H → E) '' I.source
Tactic: rw [← image_univ, ← 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
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
have h₁ : a • u = a • u
Tactic: convert! hs hu hv ha hb hab using 2
-- 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
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
⊢ a • u + b • v ∈ s
have h₂ : b • v = b • v
Tactic: convert! hs hu hv ha hb hab using 2
-- 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
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 = a • u
have h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u = a • u
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @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
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
⊢ a • u = a • u
have h₂ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u =
  HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) a : 𝕜) u
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @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
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
⊢ b • v = b • v
have h₁ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v = b • v
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @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
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
⊢ b • v = b • v
have h₂ : HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v =
  HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) b : 𝕜) v
Tactic: rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
have rw : range (↑φ : H → E) = (↑φ : H → E) '' φ.source
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ range (↑φ : H → E) = φ.target
have rw₁ : range (↑φ : H → E) = (↑φ : H → E) '' univ
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ range (↑φ : H → E) = φ.target
have rw₂ : (↑φ : H → E) '' univ = (↑φ : H → E) '' univ
Tactic: rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
⊢ if h : IsRCLikeNormedField ℝ then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ
have this : range (↑φ : H → E) = φ.target
Tactic: have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
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
⊢ if h : IsRCLikeNormedField ℝ then Convex ℝ (range (↑φ : H → E)) else range (↑φ : H → E) = univ
have simp : Convex ℝ φ.target
Tactic: simp only [instIsRCLikeNormedField, ↓reduceDIte, this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
⊢ (interior (range (↑φ : H → E))).Nonempty
have this : range (↑φ : H → E) = φ.target
Tactic: have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.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
inst_4 : NormedSpace ℝ E
⊢ Convex ℝ (range (↑I : H → E))
have pos : ∀ (h : IsRCLikeNormedField 𝕜), Convex ℝ (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
inst_4 : NormedSpace ℝ E
pos : ∀ (h : IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E))
⊢ Convex ℝ (range (↑I : H → E))
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E))
Tactic: by_cases h : IsRCLikeNormedField 𝕜
-- 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
inst_4 : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ Convex ℝ (range (↑I : H → E))
have W : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I.toPartialEquiv : H → E))
else range (↑I.toPartialEquiv : H → E) = univ
Tactic: have W := I.convex_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
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))
have W₁ : Convex ℝ (range (↑I : H → E))
Tactic: simp only [h, ↓reduceDIte, toPartialEquiv_coe] at W
Cleared hypotheses: W
-- 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 + b • v ∈ range (↑I : H → E)
have h₁ : a • u = a • u
Tactic: convert! W hu hv ha hb hab using 2
-- 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
h₁ : a • u = a • u
⊢ a • u + b • v ∈ range (↑I : H → E)
have h₂ : b • v = b • v
Tactic: convert! W hu hv ha hb hab using 2