awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
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) | x < (↑z : ℝ)}
    (Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) z hz)
⊢ Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
      (max
        (y -
          ofLp (p := 2)
            (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
                  (toLp 2 fun (x_2 : Fin 1) ↦ y - (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y) z hz) : ℝ)) ⋯) :
              EuclideanSpace ℝ (Fin 1))
            0)
        x)
      ⋯ =
    Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ 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_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
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_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      ⋯)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
have rw : (toLp 2 fun (x_2 : Fin 1) ↦
    y -
      (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
            (max
              (y -
                (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                      EuclideanSpace ℝ (Fin 1)).ofLp
                  0)
              x)
            sorry) :
        ℝ)) =
  z
Tactic: rw [Subtype.mk_eq_mk]
-- 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 : 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_2 : Fin 1) ↦
      y -
        (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
              (max
                (y -
                  (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0)
                x)
              ⋯) :
          ℝ)) =
    z
have h₁ : ∀ (i : Fin 1),
  ofLp (p := 2)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                sorry) :
            ℝ))
      i =
    z.ofLp 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)
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 ≤ y - z.ofLp 0
have linarith : y - z.ofLp 0 < x → z.ofLp 0 - (y - x) + (y - z.ofLp 0 - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
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_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      i =
    z.ofLp i
have A : x ≤ y - z.ofLp 0
Tactic: have A : x ≤ y - z 0 := by linarith
-- 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 : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ ofLp (p := 2)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      i =
    z.ofLp i
have h₁ : ofLp (p := 2)
    (toLp 2 fun (x_2 : Fin 1) ↦
      y -
        (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
              (max
                (y -
                  (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0)
                x)
              sorry) :
          ℝ))
    0 =
  z.ofLp 0
Tactic: rw [Subsingleton.elim i 0]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
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_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
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)
⊢ (↑((IccRightChart 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 [IccRightChart, 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))))
    ((↑((IccRightChart 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 [IccRightChart_extend_top, 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))))
    ((↑((IccRightChart 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 [IccRightChart_extend_top, 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))))
    ((↑((IccRightChart 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 [IccRightChart_extend_top, 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))))
    ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)
have rw₃ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 0
Tactic: rw [IccRightChart_extend_top, 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)
z : (↑(Icc x y) : Type)
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
have pos : ∀ (h' : (↑z : ℝ) < y), z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
Tactic: by_cases h' : z.val < y
-- 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 : (↑(Icc x y) : Type)
pos : ∀ (h' : (↑z : ℝ) < y), z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
have neg : ∀ (h' : ¬(↑z : ℝ) < y), z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
Tactic: by_cases h' : z.val < y
-- 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 : (↑(Icc x y) : Type)
h' : (↑z : ℝ) < y
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
have pos : z ∈ (IccLeftChart x y).source
Tactic: simp only [h', if_true]
-- 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 : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
have neg : z ∈ (IccRightChart x y).source
Tactic: simp only [h', if_false]
-- 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 : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
⊢ z ∈ (IccRightChart x y).source
have neg : y ≤ (↑z : ℝ)
Tactic: apply lt_of_lt_of_le h.out
-- 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 : (↑(Icc x y) : Type)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
have pos : ∀ (h' : (↑z : ℝ) < y),
  Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
Tactic: by_cases h' : (z : ℝ) < y
-- 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 : (↑(Icc x y) : Type)
pos :
  ∀ (h' : (↑z : ℝ) < y),
    Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
      {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
have neg : ∀ (h' : ¬(↑z : ℝ) < y),
  Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
Tactic: by_cases h' : (z : ℝ) < y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ ModelWithCorners.IsBoundaryPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M :=
    (↑(Icc x y) : Type)) ⊥
have rw : 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)) ⊥)
Tactic: rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ ModelWithCorners.IsBoundaryPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M :=
    (↑(Icc x y) : Type)) ⊤
have rw : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
  (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
  ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)
Tactic: rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_top_le (by simp)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : x < (↑p : ℝ) ∧ (↑p : ℝ) < y
⊢ ModelWithCorners.IsInteriorPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) p
have rw : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 < y.ofLp 0}
  ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) p)
Tactic: rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
    interior_range_modelWithCornersEuclideanHalfSpace]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Eq (α := Set (↑(Icc x y) : Type))
    (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type))
    {⊥, ⊤}
have h : ∀ (p : (↑(Icc x y) : Type)),
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h : ∀ (hp : (↑p : ℝ) = x),
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
h :
  ∀ (hp : (↑p : ℝ) = x),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h₁ : ∀ (hp : (↑p : ℝ) = y),
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
h :
  ∀ (hp : (↑p : ℝ) = x),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
h₁ :
  ∀ (hp : (↑p : ℝ) = y),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h₂ : ∀ (hp : (↑p : ℝ) ∈ Ioo x y),
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
Tactic: rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = x
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have this : p = ⊥
Tactic: have : p = ⊥ := SetCoe.ext hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = x
this : p = ⊥
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h : Membership.mem (γ := Set (↑(Icc x y) : Type))
    (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type))
    ⊥ ↔
  Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊥
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = y
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have this : p = ⊤
Tactic: have : p = ⊤ := SetCoe.ext hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = y
this : p = ⊤
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h : Membership.mem (γ := Set (↑(Icc x y) : Type))
    (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type))
    ⊤ ↔
  Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) ∈ Ioo x y
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h : p ∉
  ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
    (↑(Icc x y) : Type)
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) ∈ Ioo x y
h :
  p ∉
    ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type)
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
have h₁ : p ∉ {⊥, ⊤}
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
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 : I.Boundaryless
⊢ Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type)))
    (ModelWithCorners.boundary.{0, u_1, u_2, u_3} (𝕜 := ℝ) (E := E × EuclideanSpace ℝ (Fin 1)) (H :=
      ModelProd H (EuclideanHalfSpace 1)) (I := I.prod (𝓡∂ 1)) (M × (↑(Icc x y) : Type)))
    (prod univ {⊥, ⊤})
have rw : Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type)))
  (prod univ
    (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type)))
  (prod univ {⊥, ⊤})
Tactic: rw [I.boundary_of_boundaryless_left, boundary_Icc]