awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y)
    (range (ι := EuclideanHalfSpace 1) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)))
    (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
have pos : ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y)
  {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
Tactic: rw [Subtype.range_val_subtype]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
have this : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
Tactic: have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z 0 + x) := by fun_prop
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
have pos : Filter.EventuallyEq (β := (fun (x : Fin 1) ↦ ℝ) 0)
  (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
  (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
  z.ofLp 0 + x
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
pos :
  Filter.EventuallyEq (β := (fun (x : Fin 1) ↦ ℝ) 0)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    z.ofLp 0 + x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
have pos₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
  (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
⊢ Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
have apply : Membership.mem (γ := Set (PiLp 2 fun (i : Fin 1) ↦ ℝ)) {b : PiLp 2 fun (i : Fin 1) ↦ ℝ | b.ofLp 0 < y - x}
  (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x)
Tactic: apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
⊢ Filter.EventuallyEq (β := (fun (x : Fin 1) ↦ ℝ) 0)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    z.ofLp 0 + x
have this₁ : Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x))
  {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
Tactic: have : {w : EuclideanSpace ℝ (Fin 1) | w 0 < y - x} ∈ 𝓝 (toLp 2 fun i ↦ z - x) := by
      apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds
      simpa using hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this_1 : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
⊢ Filter.EventuallyEq (β := (fun (x : Fin 1) ↦ ℝ) 0)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ min (max (x_1.ofLp 0) 0 + x) y) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    z.ofLp 0 + x
have h₁ : ∀ (w : EuclideanSpace ℝ (Fin 1)) (hw : 0 ≤ w.ofLp 0) (h'w : w.ofLp 0 < y - x),
  min (max (w.ofLp 0) 0 + x) y = w.ofLp 0 + x
Tactic: filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this_1 : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
w : EuclideanSpace ℝ (Fin 1)
hw : 0 ≤ w.ofLp 0
h'w : w.ofLp 0 < y - x
⊢ min (max (w.ofLp 0) 0 + x) y = w.ofLp 0 + x
have h₁ : w.ofLp 0 + x ≤ y
Tactic: rw [max_eq_left hw, min_eq_left]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
this_1 : ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ (↑z : ℝ) - x))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
w : EuclideanSpace ℝ (Fin 1)
hw : 0 ≤ w.ofLp 0
h'w : w.ofLp 0 < y - x
⊢ w.ofLp 0 + x ≤ y
have linarith : y < w.ofLp 0 + x → w.ofLp 0 - (y - x) + (y - (w.ofLp 0 + x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : ¬(↑z : ℝ) < y
⊢ ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(IccRightChart x y).symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      ((↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1) z))
have hz₁ : y ≤ (↑z : ℝ)
Tactic: simp only [not_lt] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x)
    (range (ι := EuclideanHalfSpace 1) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)))
    (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
have neg : ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x)
  {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
Tactic: rw [Subtype.range_val_subtype]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
have this : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
Tactic: have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z 0) := by fun_prop
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
have neg : Filter.EventuallyEq (β := ℝ) (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
  (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
  y - z.ofLp 0
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
neg :
  Filter.EventuallyEq (β := ℝ)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    y - z.ofLp 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x)
    {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0} (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
have neg₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
  (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
⊢ Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ)))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
have apply : Membership.mem (γ := Set (PiLp 2 fun (i : Fin 1) ↦ ℝ)) {b : PiLp 2 fun (i : Fin 1) ↦ ℝ | b.ofLp 0 < y - x}
  (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ))
Tactic: apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
⊢ Filter.EventuallyEq (β := ℝ)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    y - z.ofLp 0
have this₁ : Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ)))
  {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
Tactic: have : {w : EuclideanSpace ℝ (Fin 1) | w 0 < y - x} ∈ 𝓝 (toLp 2 fun i ↦ y - z) := by
      apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds
      simpa using h.out.trans_le hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this_1 : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ)))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
⊢ Filter.EventuallyEq (β := ℝ)
    (𝓝[{x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}] toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))
    (fun (x_1 : EuclideanSpace ℝ (Fin 1)) ↦ max (y - max (x_1.ofLp 0) 0) x) fun (z : EuclideanSpace ℝ (Fin 1)) ↦
    y - z.ofLp 0
have h₁ : ∀ (w : EuclideanSpace ℝ (Fin 1)) (hw : 0 ≤ w.ofLp 0) (h'w : w.ofLp 0 < y - x),
  max (y - max (w.ofLp 0) 0) x = y - w.ofLp 0
Tactic: filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this_1 : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ)))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
w : EuclideanSpace ℝ (Fin 1)
hw : 0 ≤ w.ofLp 0
h'w : w.ofLp 0 < y - x
⊢ max (y - max (w.ofLp 0) 0) x = y - w.ofLp 0
have h₁ : x ≤ y - w.ofLp 0
Tactic: rw [max_eq_left hw, max_eq_left]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
this_1 : ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0
this :
  Membership.mem (γ := Filter (WithLp 2 ((i : Fin 1) → ℝ))) (𝓝 (toLp 2 fun (i : Fin 1) ↦ y - (↑z : ℝ)))
    {w : EuclideanSpace ℝ (Fin 1) | w.ofLp 0 < y - x}
w : EuclideanSpace ℝ (Fin 1)
hw : 0 ≤ w.ofLp 0
h'w : w.ofLp 0 < y - x
⊢ x ≤ y - w.ofLp 0
have linarith : y - w.ofLp 0 < x → w.ofLp 0 - (y - x) + (y - w.ofLp 0 - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContMDiffWithinAt 𝓘(ℝ, ℝ) (E' := EuclideanSpace ℝ (Fin 1)) (H' := EuclideanHalfSpace 1) (𝓡∂ 1) n (projIcc x y ⋯)
    (Icc x y) z
have rw : ContinuousWithinAt (projIcc x y sorry) (Icc x y) z ∧
  ContDiffWithinAt ℝ (F := EuclideanSpace ℝ (Fin 1)) n
    ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y sorry z)) :
        (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ∘
      projIcc x y sorry ∘ (↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ))
    ((↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ) ⁻¹' Icc x y ∩ range (↑𝓘(ℝ, ℝ) : ℝ → ℝ))
    ((↑(extChartAt 𝓘(ℝ, ℝ) z) : ℝ → ℝ) z)
Tactic: rw [contMDiffWithinAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContinuousWithinAt (projIcc x y ⋯) (Icc x y) z
have h₁ : ContinuousAt (projIcc x y sorry) z
Tactic: apply ContinuousAt.continuousWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContinuousWithinAt (projIcc x y ⋯) (Icc x y) z ∧
    ContDiffWithinAt ℝ (F := EuclideanSpace ℝ (Fin 1)) n
      ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ z)) :
          (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ∘
        projIcc x y ⋯ ∘ (↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ))
      ((↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ) ⁻¹' Icc x y ∩ range (↑𝓘(ℝ, ℝ) : ℝ → ℝ))
      ((↑(extChartAt 𝓘(ℝ, ℝ) z) : ℝ → ℝ) z)
have refine : ContDiffWithinAt ℝ (F := EuclideanSpace ℝ (Fin 1)) n
  ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y sorry z)) :
      (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ∘
    projIcc x y sorry ∘ (↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ))
  ((↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ) ⁻¹' Icc x y ∩ range (↑𝓘(ℝ, ℝ) : ℝ → ℝ)) ((↑(extChartAt 𝓘(ℝ, ℝ) z) : ℝ → ℝ) z)
Tactic: refine ⟨by apply ContinuousAt.continuousWithinAt; fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContDiffWithinAt ℝ (F := EuclideanSpace ℝ (Fin 1)) n
    ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ z)) :
        (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ∘
      projIcc x y ⋯ ∘ (↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ))
    ((↑(extChartAt 𝓘(ℝ, ℝ) z).symm : ℝ → ℝ) ⁻¹' Icc x y ∩ range (↑𝓘(ℝ, ℝ) : ℝ → ℝ))
    ((↑(extChartAt 𝓘(ℝ, ℝ) z) : ℝ → ℝ) z)
have suffices : ContDiffWithinAt ℝ n
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑(if (↑(projIcc x y sorry z) : ℝ) < y then IccLeftChart x y else IccRightChart x y) :
        (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
    projIcc x y sorry)
  (Icc x y) z
Tactic: suffices ContDiffWithinAt ℝ n _ (Icc x y) z by simpa
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(if (↑(projIcc x y ⋯ z) : ℝ) < y then IccLeftChart x y else IccRightChart x y) :
          (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have pos : ∀ (h'z : (↑(projIcc x y sorry z) : ℝ) < y),
  ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y sorry)
    (Icc x y) z
Tactic: split_ifs with h'z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
pos :
  ∀ (h'z : (↑(projIcc x y ⋯ z) : ℝ) < y),
    ContDiffWithinAt ℝ n
      (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
        projIcc x y ⋯)
      (Icc x y) z
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(if (↑(projIcc x y ⋯ z) : ℝ) < y then IccLeftChart x y else IccRightChart x y) :
          (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have neg : ∀ (h'z : ¬(↑(projIcc x y sorry z) : ℝ) < y),
  ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y sorry)
    (Icc x y) z
Tactic: split_ifs with h'z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have this : ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
  have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
  this
Tactic: have : ContDiff ℝ n (fun (w : ℝ) ↦
        (show EuclideanSpace ℝ (Fin 1) from toLp 2 fun (_ : Fin 1) ↦ w - x)) := by
      dsimp
      apply contDiff_euclidean.2 (fun i ↦ by fun_prop)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
this :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have apply : ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
    projIcc x y sorry =ᶠ[𝓝[Icc x y] z]
  fun (w : ℝ) ↦
  have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
  this
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem _ hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
this :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯ =ᶠ[𝓝[Icc x y] z]
    fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
have h₁ : ∀ (w : ℝ) (hw : w ∈ Icc x y),
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
        projIcc x y sorry)
      w =
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
Tactic: filter_upwards [self_mem_nhdsWithin] with w hw
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
this :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
        projIcc x y ⋯)
      w =
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
have h₁ : ∀ (i : Fin 1),
  ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
            projIcc x y sorry)
          w).ofLp
      i =
    ofLp (p := 2)
      (have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
      this)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
this :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ max x (min y w) - x = w - x
have h₁ : x ≤ min y w
Tactic: rw [max_eq_right, min_eq_right hw.2]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬(↑(projIcc x y ⋯ z) : ℝ) < y
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have this : ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
  have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
  this
Tactic: have : ContDiff ℝ n (fun (w : ℝ) ↦
        (show EuclideanSpace ℝ (Fin 1) from toLp 2 fun (_ : Fin 1) ↦ y - w)) := by
      dsimp
      apply contDiff_euclidean.2 (fun i ↦ by fun_prop)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬(↑(projIcc x y ⋯ z) : ℝ) < y
this :
  ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
    this
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z
have apply : ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
    projIcc x y sorry =ᶠ[𝓝[Icc x y] z]
  fun (w : ℝ) ↦
  have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
  this
Tactic: apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem _ hz