awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
this :
  ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(if (↑z : ℝ) < y then IccLeftChart x y else 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))
      ((↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)
        z))
⊢ ContDiffWithinAt ℝ (E := EuclideanSpace ℝ (Fin 1)) n
    ((↑(extChartAt 𝓘(ℝ, ℝ) (↑z : ℝ)) : ℝ → ℝ) ∘
      (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
        (↑(PartialEquiv.symm (extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z)) :
          EuclideanSpace ℝ (Fin 1) → (↑(Icc x y) : Type)))
    (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
    ((↑(extChartAt (H := EuclideanHalfSpace 1) (𝓡∂ 1) z) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) z)

Tactic:
simpa
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
pos :
  ∀ (hz : (↑z : ℝ) < y),
    ContDiffWithinAt ℝ (F := ℝ) n
      ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
        (↑(IccLeftChart 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))
        ((↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1) z))
neg :
  ∀ (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))
⊢ ContDiffWithinAt ℝ (F := ℝ) n
    ((fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) ∘
      (↑(if (↑z : ℝ) < y then IccLeftChart x y else 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))
      ((↑(if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)
        z))

Tactic:
split_ifs with hz
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
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)
⊢ 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)

Tactic:
rw [Subtype.range_val_subtype]

Premises used: Subtype.range_val_subtype
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
⊢ ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) 0) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z.ofLp 0 + x

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : (↑z : ℝ) < y
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
pos₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
    (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - 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)

Tactic:
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_of_mem, ContDiff.contDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
    (toLp 2 fun (x_1 : Fin 1) ↦ (↑z : ℝ) - x)

Tactic:
simpa using z.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
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)
⊢ 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:
apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds

Premises used: isOpen_lt, continuous_const, PiLp.continuous_apply, IsOpen.mem_nhds, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 (γ := 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:
simpa using hz
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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}

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
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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}
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
⊢ 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:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w

Premises used: nhdsWithin_le_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : w.ofLp 0 + x ≤ y
⊢ min (max (w.ofLp 0) 0 + x) y = w.ofLp 0 + x

Tactic:
rw [max_eq_left hw, min_eq_left]

Premises used: max_eq_left, min_eq_left
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
linarith : y < w.ofLp 0 + x → w.ofLp 0 - (y - x) + (y - (w.ofLp 0 + x)) = 0
⊢ w.ofLp 0 + x ≤ y

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : ¬(↑z : ℝ) < y
⊢ y ≤ (↑z : ℝ)

Tactic:
simp only [not_lt] at hz

Premises used: not_lt
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
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 : ℝ))
⊢ 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 : ℝ))

Tactic:
rw [Subtype.range_val_subtype]

Premises used: Subtype.range_val_subtype
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
⊢ ContDiff ℝ (F := ℝ) n fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z.ofLp 0

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : (↑(Icc x y) : Type)
hz : y ≤ (↑z : ℝ)
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
neg₁ :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
    (toLp 2 fun (x_1 : Fin 1) ↦ 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 : ℝ))

Tactic:
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_of_mem, ContDiff.contDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 (γ := Set (EuclideanSpace ℝ (Fin 1))) {x : EuclideanSpace ℝ (Fin 1) | 0 ≤ x.ofLp 0}
    (toLp 2 fun (x_1 : Fin 1) ↦ y - (↑z : ℝ))

Tactic:
simpa using z.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
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 : ℝ))
⊢ 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:
apply (isOpen_lt (PiLp.continuous_apply 2 _ 0) continuous_const).mem_nhds

Premises used: isOpen_lt, continuous_const, PiLp.continuous_apply, IsOpen.mem_nhds, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 (γ := 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:
simpa using h.out.trans_le hz

Premises used: LT.lt.trans_le, Fact.out
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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}

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
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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}
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
⊢ 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:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w

Premises used: nhdsWithin_le_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : x ≤ y - w.ofLp 0
⊢ max (y - max (w.ofLp 0) 0) x = y - w.ofLp 0

Tactic:
rw [max_eq_left hw, max_eq_left]

Premises used: max_eq_left
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
linarith : y - w.ofLp 0 < x → w.ofLp 0 - (y - x) + (y - w.ofLp 0 - x) = 0
⊢ x ≤ y - w.ofLp 0

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
rw :
  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)
⊢ ContMDiffWithinAt 𝓘(ℝ, ℝ) (E' := EuclideanSpace ℝ (Fin 1)) (H' := EuclideanHalfSpace 1) (𝓡∂ 1) n (projIcc x y ⋯)
    (Icc x y) z

Tactic:
rw [contMDiffWithinAt_iff]

Premises used: contMDiffWithinAt_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h₁ : ContinuousAt (projIcc x y ⋯) z
⊢ ContinuousWithinAt (projIcc x y ⋯) (Icc x y) z

Tactic:
apply ContinuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
⊢ ContinuousAt (projIcc x y ⋯) z

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
refine :
  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)
⊢ 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)

Tactic:
refine ⟨by apply ContinuousAt.continuousWithinAt; fun_prop, ?_⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
this :
  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
⊢ 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)

Tactic:
simpa
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
suffices :
  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
⊢ 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)

Tactic:
suffices ContDiffWithinAt ℝ n _ (Icc x y) z by simpa
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
neg :
  ∀ (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
⊢ 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

Tactic:
split_ifs with h'z
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
i : Fin 1
⊢ ContDiff ℝ (F := (fun (x : Fin 1) ↦ ℝ) i) n fun (x_1 : ℝ) ↦ ofLp (p := 2) (toLp 2 fun (x_2 : Fin 1) ↦ x_1 - x) i

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
⊢ ContDiff ℝ (F := EuclideanSpace ℝ (Fin 1)) n fun (w : ℝ) ↦ toLp 2 fun (x_1 : Fin 1) ↦ w - x

Tactic:
apply contDiff_euclidean.2 (fun i ↦ by fun_prop)

Premises used: Iff.mpr, contDiff_euclidean
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : (↑(projIcc x y ⋯ z) : ℝ) < y
⊢ 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)
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
apply :
  ((↑(𝓡∂ 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
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
      projIcc x y ⋯)
    (Icc x y) z

Tactic:
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem _ hz

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_of_mem, ContDiff.contDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
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 ⋯)
        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

Tactic:
filter_upwards [self_mem_nhdsWithin] with w hw

Premises used: self_mem_nhdsWithin