awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : x < min (z.ofLp 0 + x) y
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have hz₃ : 0 < z.ofLp 0
Tactic: rw [min_eq_left hz₁.le, lt_add_iff_pos_left] at hz₂
Cleared hypotheses: hz₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have h : ∀ (i : Fin 1),
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i
have h : (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
            (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
    0 =
  ofLp (p := 2)
    ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
    0
Tactic: rw [Subsingleton.elim i 0]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0
have h : y - (z.ofLp 0 + x) = -z.ofLp 0 + (y - x)
Tactic: simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, *,
      max_eq_left, min_eq_left hz₁.le, update_self, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h : ∀
  x_2 ∈
    (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)),
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      x_2 =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      x_2
Tactic: apply M.contDiffOn.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (IccRightChart x y).symm.symm.target
hz₂ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (↑(IccRightChart x y).symm.symm.symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ⁻¹' (IccLeftChart x y).source
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have hz₃ : z.ofLp 0 < y - x
Tactic: simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff,
      update_self, max_eq_left hz₀, mfld_simps] at hz₁ hz₂
Cleared hypotheses: hz₁, hz₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (IccRightChart x y).symm.symm.target
hz₂ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (↑(IccRightChart x y).symm.symm.symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ⁻¹' (IccLeftChart x y).source
hz₃ : z.ofLp 0 < y - x
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have hz₄ : y - z.ofLp 0 < y ∧ x < y
Tactic: simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff,
      update_self, max_eq_left hz₀, mfld_simps] at hz₁ hz₂
Cleared hypotheses: hz₁, hz₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 < y - x
hz₂ : y - z.ofLp 0 < y ∧ x < y
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have hz₃ : x < y - z.ofLp 0
Tactic: rw [lt_sub_comm] at hz₁
Cleared hypotheses: hz₁, hz₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))
have h : ∀ (i : Fin 1),
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i
have h : (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
            (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
    0 =
  ofLp (p := 2)
    ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
    0
Tactic: rw [Subsingleton.elim i 0]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0
have h : y - z.ofLp 0 - x = -z.ofLp 0 + (y - x)
Tactic: simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart,
      update_self, max_eq_left, hz₀, hz₁.le, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ContDiffOn ℝ (F := ↥(ℝ ∙ v)ᗮ) n (stereoToFun v)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
have refine : ContDiffOn ℝ (F := ℝ) n
  (fun (i : E) ↦
    2 / HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) i : ℝ))
  {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
Tactic: refine ContDiffOn.fun_smul ?_ (ℝ ∙ v)ᗮ.orthogonalProjection.contDiff.contDiffOn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ContDiffOn ℝ (F := ℝ) n
    (fun (i : E) ↦
      2 / HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) i : ℝ))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
have refine_1 : ContDiffOn ℝ (F := ℝ) n
  (fun (i : E) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) i : ℝ))
  {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
Tactic: refine contDiff_const.contDiffOn.div ?_ ?_