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 : ℝ
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
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccRightChart 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 : Fin 1) ↦ y - w;
    this
have h₁ : ∀ (w : ℝ) (hw : w ∈ Icc x y),
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
        projIcc x y sorry)
      w =
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
    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 : Fin 1) ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
        projIcc x y ⋯)
      w =
    have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
    this
have h₁ : ∀ (i : Fin 1),
  ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑(IccRightChart 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 : Fin 1) ↦ y - w;
      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 : Fin 1) ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ y - max x (min y w) = y - w
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 (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↔
    ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f
have refine : ∀ (hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y sorry) (Icc x y)),
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffOn contMDiffOn_projIcc⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f
have h₁ : f = (f ∘ projIcc x y sorry) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)
Tactic: convert! hf.comp_contMDiff (contMDiff_subtype_coe_Icc (x := x) (y := y)) (fun z ↦ z.2)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)
⊢ f = (f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)
have h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y sorry) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
⊢ ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) ↔
    ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f w
have refine : ∀ (hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y sorry) (Icc x y) (↑w : ℝ)),
  ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f w
Tactic: refine ⟨fun hf ↦ ?_,
    fun hf ↦ hf.comp_contMDiffWithinAt_of_eq (contMDiffOn_projIcc w w.2) (by simp)⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ)
⊢ ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f w
have A : ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
  (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
Tactic: have A := contMDiff_subtype_coe_Icc (x := x) (y := y) (n := n) w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ)
A :
  ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
⊢ ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f w
have A₁ : ContMDiffWithinAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
  (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) univ w
Tactic: rw [← contMDiffWithinAt_univ] at A ⊢
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ)
A :
  ContMDiffWithinAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) univ w
⊢ ContMDiffWithinAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f univ w
have h₁ : f = (f ∘ projIcc x y sorry) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
Tactic: convert! hf.comp _ A (fun z hz ↦ z.2)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ)
A :
  ContMDiffWithinAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) univ w
⊢ f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
have h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y sorry) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ) ↔ MDiffAt f w
have refine_1 : ∀ (hf : MDiffAt[Icc x y] (f ∘ projIcc x y sorry) (↑w : ℝ)), MDiffAt f w
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
refine_1 : ∀ (hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)), MDiffAt f w
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ) ↔ MDiffAt f w
have refine_2 : ∀ (hf : MDiffAt f w), MDiffAt[Icc x y] (f ∘ projIcc x y sorry) (↑w : ℝ)
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
⊢ MDiffAt f w
have A : (MDiffAt fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
Tactic: have A := (contMDiff_subtype_coe_Icc (x := x) (y := y) w).mdifferentiableAt one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
A : (MDiffAt fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
⊢ MDiffAt f w
have A₁ : (MDiffAt[univ] fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
Tactic: rw [← mdifferentiableWithinAt_univ] at A ⊢
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
A : (MDiffAt[univ] fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
⊢ MDiffAt[univ] f w
have h₁ : f = (f ∘ projIcc x y sorry) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
Tactic: convert! hf.comp _ A (fun z hz ↦ z.2)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
A : (MDiffAt[univ] fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w
⊢ f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
have h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y sorry) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (hypothesis)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hf : MDiffAt f w
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
have this : MDiffAt[Icc x y] (projIcc x y sorry) (↑w : ℝ)
Tactic: have := (contMDiffOn_projIcc (x := x) (y := y) w w.2).mdifferentiableWithinAt one_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ Eq (α := TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ z))
    ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) z :
        (a : TangentSpace 𝓘(ℝ, ℝ) z) → TangentSpace (𝓡∂ 1) (projIcc x y ⋯ z))
      1)
    (oneTangentSpaceIcc (projIcc x y ⋯ z))
have simp : Eq (α := TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y sorry z))
  ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y sorry) (Icc x y) z :
      (a : TangentSpace 𝓘(ℝ, ℝ) z) → TangentSpace (𝓡∂ 1) (projIcc x y sorry z))
    1)
  ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y sorry) (Icc x y) (↑(projIcc x y sorry z) : ℝ) :
      (a : TangentSpace 𝓘(ℝ, ℝ) (↑(projIcc x y sorry z) : ℝ)) →
        TangentSpace (𝓡∂ 1) (projIcc x y sorry (↑(projIcc x y sorry z) : ℝ)))
    1)
Tactic: simp only [oneTangentSpaceIcc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ Eq (α := TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ z))
    ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) z :
        (a : TangentSpace 𝓘(ℝ, ℝ) z) → TangentSpace (𝓡∂ 1) (projIcc x y ⋯ z))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑(projIcc x y ⋯ z) : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑(projIcc x y ⋯ z) : ℝ)) →
          TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑(projIcc x y ⋯ z) : ℝ)))
      1)
have e_a : z = (↑(projIcc x y sorry z) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos : ∀ (hw : MDiffAt f w),
  Eq (α := TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y sorry) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
Tactic: by_cases hw : MDiffAt f w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
pos :
  ∀ (hw : MDiffAt f w),
    Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
          1 :
        TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
      ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have neg : ∀ (hw : ¬MDiffAt f w),
  Eq (α := TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y sorry) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
Tactic: by_cases hw : MDiffAt f w
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : ¬MDiffAt f w
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have neg : Eq.{u_1 + 1} (α := TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
  ((0 : (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ))) 1 :
    TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
  ((0 : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
Tactic: rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : ¬MDiffAt f w
neg :
  Eq.{u_1 + 1} (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((0 : (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ))) 1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((0 : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have neg₁ : ¬MDiffAt[Icc x y] (f ∘ projIcc x y sorry) (↑w : ℝ)
Tactic: rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos : Eq (α := TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
  ((ContinuousLinearMap.comp (M₂ :=
          TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y sorry (↑w : ℝ)))
          (mfderiv% f (projIcc x y sorry (↑w : ℝ))) (mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y sorry) (Icc x y) (↑w : ℝ)) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
      1 :
    TangentSpace I ((f ∘ projIcc x y sorry) (↑w : ℝ)))
  ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
Tactic: rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
pos :
  Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((ContinuousLinearMap.comp (M₂ :=
            TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
            (mfderiv% f (projIcc x y ⋯ (↑w : ℝ))) (mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ)) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos₁ : MDiffAt f (projIcc x y sorry (↑w : ℝ))
Tactic: rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Icc (goal)
Goal:
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
x y : ℝ
h : Fact (x < y)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
pos :
  Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((ContinuousLinearMap.comp (M₂ :=
            TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
            (mfderiv% f (projIcc x y ⋯ (↑w : ℝ))) (mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ)) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
pos₁ : MDiffAt f (projIcc x y ⋯ (↑w : ℝ))
⊢ Eq (α := TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (f ∘ projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
        1 :
      TangentSpace I ((f ∘ projIcc x y ⋯) (↑w : ℝ)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))
have pos₂ : MDiffAt[Icc x y] (projIcc x y sorry) (↑w : ℝ)
Tactic: rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]