awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), interior (f i ⁻¹' Ici a)) (⋂ (i : Fin n), f i ⁻¹' Ioi a)
have apply : ∀ (i : Fin n), interior (f i ⁻¹' Ici a) = f i ⁻¹' Ioi a
Tactic: apply iInter_congr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
i : Fin n
⊢ interior (f i ⁻¹' Ici a) = f i ⁻¹' Ioi a
have hf₂ : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
Tactic: rw [← (PiLp.isOpenMap_apply p _ i).preimage_interior_eq_interior_preimage, interior_Ici]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
x : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
h :
  Membership.mem (γ := Set (EuclideanHalfSpace n)) univ
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)
⊢ Eq (α := EuclideanHalfSpace n)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2
        (update (β := fun (x : Fin n) ↦ ℝ)
          (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          0
          (max
            ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
                  EuclideanSpace ℝ (Fin n)).ofLp
              0)
            0)))
      ⋯)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)
have rw : max
      ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
            EuclideanSpace ℝ (Fin n)).ofLp
        0)
      0 =
    (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
        (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
      xval 0 ∧
  ∀ (x : Fin n),
    x ≠ 0 →
      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          x =
        (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
            (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
          xval x
Tactic: rw [Subtype.mk_eq_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
⊢ (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)
          (toLp 2 (update (β := fun (x : Fin n) ↦ ℝ) x.ofLp 0 (max (x.ofLp 0) 0))) ⋯) :
      EuclideanSpace ℝ (Fin n)) =
    x
have rw : max (x.ofLp 0) 0 =
    (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
        (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
      x 0 ∧
  ∀ (x_1 : Fin n),
    x_1 ≠ 0 →
      x.ofLp x_1 =
        (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
            (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
          x x_1
Tactic: rw [Subtype.coe_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ if h : IsRCLikeNormedField ℝ then
    Convex ℝ (E := EuclideanSpace ℝ (Fin n))
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
  else
    Eq (α := Set (EuclideanSpace ℝ (Fin n)))
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0))) univ
have simp : Convex ℝ (E := EuclideanSpace ℝ (Fin n))
  (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
Tactic: simp only [instIsRCLikeNormedField, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
have hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n))
  (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
Tactic: apply Convex.convex_isRCLikeNormedField
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
have hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
Tactic: rw [range_euclideanHalfSpace n]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n))
    (interior
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0))))
have rw : Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | 0 < y.ofLp 0}
Tactic: rw [range_euclideanHalfSpace, interior_halfSpace]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
x : EuclideanQuadrant n
h : Membership.mem (γ := Set (EuclideanQuadrant n)) univ x
⊢ Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
      (toLp 2 fun (i : Fin n) ↦ max ((↑x : EuclideanSpace ℝ (Fin n)).ofLp i) 0) ⋯ =
    x
have h : ∀ (i : Fin n),
  ofLp (p := 2)
      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
            (toLp 2 fun (i : Fin n) ↦ max ((↑x : EuclideanSpace ℝ (Fin n)).ofLp i) 0) sorry) :
        EuclideanSpace ℝ (Fin n))
      i =
    (↑x : EuclideanSpace ℝ (Fin n)).ofLp i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x
⊢ (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
          (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) ⋯) :
      EuclideanSpace ℝ (Fin n)) =
    x
have h : ∀ (i : Fin n),
  ofLp (p := 2)
      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
            (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) sorry) :
        EuclideanSpace ℝ (Fin n))
      i =
    x.ofLp i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
⊢ if h : IsRCLikeNormedField ℝ then
    Convex ℝ (E := EuclideanSpace ℝ (Fin n))
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
  else
    Eq (α := Set (EuclideanSpace ℝ (Fin n)))
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
      univ
have simp : Convex ℝ (E := EuclideanSpace ℝ (Fin n))
  (range (ι := EuclideanQuadrant n)
    (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
Tactic: simp only [instIsRCLikeNormedField, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
have hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n))
  (range (ι := EuclideanQuadrant n)
    (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
Tactic: apply Convex.convex_isRCLikeNormedField
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
have hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}
Tactic: rw [range_euclideanQuadrant]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n))
    (interior
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i))))
have rw : Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), 0 < y.ofLp i}
Tactic: rw [range_euclideanQuadrant, interior_euclideanQuadrant]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    interior {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
have h : range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
  {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
Tactic: congr!
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    {y : EuclideanSpace ℝ (Fin n) | 0 < y.ofLp 0}
have calc : interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
  interior {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
Tactic: calc interior (range (𝓡∂ n))
    _ = interior ({ y | 0 ≤ y 0}) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 < y 0 } := interior_halfSpace _ _ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    frontier {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
have h : range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
  {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
Tactic: congr!
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    {y : EuclideanSpace ℝ (Fin n) | 0 = y.ofLp 0}
have calc : frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
  frontier {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
Tactic: calc frontier (range (𝓡∂ n))
    _ = frontier ({ y | 0 ≤ y 0 }) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 = y 0 } := frontier_halfSpace 2 _ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    Membership.mem (γ := Set (EuclideanHalfSpace 1))
        {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x} x_1 →
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | (↑z : ℝ) < y}
        (Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) (min ((↑x_1 : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x) y) ⋯)
have simp : ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
  (↑x_1 : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x → (↑x_1 : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x < y ∨ y < y
Tactic: simp only [min_lt_iff, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x
⊢ (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x < y ∨ y < y
have h₁ : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x < y
Tactic: left
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x
⊢ (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x < y
have linarith : y ≤ (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x →
  (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 - (y - x) + (y - ((↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z :
  Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | (↑z : ℝ) < y}
    (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) z hz)
⊢ Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
      (min
        (ofLp (p := 2)
            (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
                  (toLp 2 fun (x_1 : Fin 1) ↦ (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) z hz) : ℝ) - x) ⋯) :
              EuclideanSpace ℝ (Fin 1))
            0 +
          x)
        y)
      ⋯ =
    Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) z hz
have hz₁ : x ≤ z ∧ z ≤ y
Tactic: simp only [mem_setOf_eq, mem_Icc] at hz h'z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z :
  Membership.mem (γ := Set (EuclideanHalfSpace 1))
    {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
⊢ Eq (α := EuclideanHalfSpace 1)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2 fun (x_1 : Fin 1) ↦
        (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                (min
                  ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0 +
                    x)
                  y)
                ⋯) :
            ℝ) -
          x)
      ⋯)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
have rw : (toLp 2 fun (x_1 : Fin 1) ↦
    (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
            (min
              ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                      EuclideanSpace ℝ (Fin 1)).ofLp
                  0 +
                x)
              y)
            sorry) :
        ℝ) -
      x) =
  z
Tactic: rw [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z :
  Membership.mem (γ := Set (EuclideanHalfSpace 1))
    {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
⊢ (toLp 2 fun (x_1 : Fin 1) ↦
      (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
              (min
                ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0 +
                  x)
                y)
              ⋯) :
          ℝ) -
        x) =
    z
have h₁ : ∀ (i : Fin 1),
  ofLp (p := 2)
      (toLp 2 fun (x_1 : Fin 1) ↦
        (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                (min
                  ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0 +
                    x)
                  y)
                sorry) :
            ℝ) -
          x)
      i =
    z.ofLp i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
⊢ x + z.ofLp 0 ≤ y
have linarith : y < x + z.ofLp 0 → z.ofLp 0 - (y - x) + (y - (x + z.ofLp 0)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
⊢ ofLp (p := 2)
      (toLp 2 fun (x_1 : Fin 1) ↦
        (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                (min
                  ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0 +
                    x)
                  y)
                ⋯) :
            ℝ) -
          x)
      i =
    z.ofLp i
have A : x + z.ofLp 0 ≤ y
Tactic: have A : x + z 0 ≤ y := by linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x + z.ofLp 0 ≤ y
⊢ ofLp (p := 2)
      (toLp 2 fun (x_1 : Fin 1) ↦
        (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                (min
                  ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0 +
                    x)
                  y)
                ⋯) :
            ℝ) -
          x)
      i =
    z.ofLp i
have h₁ : ofLp (p := 2)
    (toLp 2 fun (x_1 : Fin 1) ↦
      (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
              (min
                ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0 +
                  x)
                y)
              sorry) :
          ℝ) -
        x)
    0 =
  z.ofLp 0
Tactic: rw [Subsingleton.elim i 0]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
⊢ IsOpen (X := EuclideanHalfSpace 1) {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
have this : IsOpen (X := ℝ) {z : ℝ | z < y - x}
Tactic: have : IsOpen { z : ℝ | z < y - x } := isOpen_Iio
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
this : IsOpen (X := ℝ) {z : ℝ | z < y - x}
⊢ IsOpen (X := EuclideanHalfSpace 1) {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
have this₁ : IsOpen (X := EuclideanSpace ℝ (Fin 1)) {z : EuclideanSpace ℝ (Fin 1) | z.ofLp 0 < y - x}
Tactic: have : IsOpen { z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x } :=
      this.preimage (@PiLp.continuous_apply 2 (Fin 1) (fun _ => ℝ) _ 0)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ (↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥ = 0
have norm_num : Eq (α := EuclideanSpace ℝ (Fin 1))
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x : Fin 1) ↦ 0) sorry))
  0
Tactic: norm_num [IccLeftChart, modelWithCornersEuclideanHalfSpace_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)
have rw : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
  (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
Tactic: rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)
have rw₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 = y.ofLp 0} 0
Tactic: rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
rw₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 = y.ofLp 0} 0
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)
have rw₂ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 (ofLp (p := 2) 0 0)
Tactic: rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
rw₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 = y.ofLp 0} 0
rw₂ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 (ofLp (p := 2) 0 0)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)
have rw₃ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 0
Tactic: rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_2 : EuclideanHalfSpace 1⦄,
    Membership.mem (γ := Set (EuclideanHalfSpace 1))
        {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x} x_2 →
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | x < (↑z : ℝ)}
        (Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y) (max (y - (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0) x) ⋯)
have simp : ∀ ⦃x_2 : EuclideanHalfSpace 1⦄,
  (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x → x < y - (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0 ∨ x < x
Tactic: simp only [lt_max_iff, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x
⊢ x < y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 ∨ x < x
have h₁ : x < y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0
Tactic: left