awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w : ℝ
hw : w ∈ Icc x y
h₁ :
  ∀ (i : Fin 1),
    ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
                (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
              projIcc x y ⋯)
            w).ofLp
        i =
      ofLp (p := 2)
        (have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
        this)
        i
⊢ (((↑(𝓡∂ 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

Tactic:
ext i
-- 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_1 :
  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
this : max x (min y w) - x = w - x
⊢ ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑(IccLeftChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
            projIcc x y ⋯)
          w).ofLp
      i =
    ofLp (p := 2)
      (have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x_1 : Fin 1) ↦ w - x;
      this)
      i

Tactic:
simpa [modelWithCornersEuclideanHalfSpace, IccLeftChart]

Premises used: modelWithCornersEuclideanHalfSpace, IccLeftChart
-- 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
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
h₁ : x ≤ min y w
⊢ max x (min y w) - x = w - x

Tactic:
rw [max_eq_right, min_eq_right hw.2]

Premises used: min_eq_right, max_eq_right, And.right
-- 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
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w

Tactic:
simp [hw.1, h.out.le]

Premises used: LT.lt.le, And.left, Fact.out
-- 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 : ℝ) ↦ ofLp (p := 2) (toLp 2 fun (x_1 : Fin 1) ↦ y - 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 : Fin 1) ↦ y - w

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 : 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)
-- 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 : Fin 1) ↦ y - w;
    this
apply :
  ((↑(𝓡∂ 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
⊢ ContDiffWithinAt ℝ n
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑(IccRightChart 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 : Fin 1) ↦ y - w;
    this
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 ⋯)
        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

Tactic:
filter_upwards [self_mem_nhdsWithin] with w hw

Premises used: self_mem_nhdsWithin
-- 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 : Fin 1) ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
h₁ :
  ∀ (i : Fin 1),
    ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
                (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
              projIcc x y ⋯)
            w).ofLp
        i =
      ofLp (p := 2)
        (have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
        this)
        i
⊢ (((↑(𝓡∂ 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

Tactic:
ext i
-- 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_1 :
  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
this : y - max x (min y w) = y - w
⊢ ((((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑(IccRightChart x y) : (↑(Icc x y) : Type) → EuclideanHalfSpace 1)) ∘
            projIcc x y ⋯)
          w).ofLp
      i =
    ofLp (p := 2)
      (have this : EuclideanSpace ℝ (Fin 1) := toLp 2 fun (x : Fin 1) ↦ y - w;
      this)
      i

Tactic:
simpa [modelWithCornersEuclideanHalfSpace, IccRightChart]

Premises used: IccRightChart, modelWithCornersEuclideanHalfSpace
-- 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 : Fin 1) ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
h₁ : x ≤ min y w
⊢ y - max x (min y w) = y - w

Tactic:
rw [max_eq_right, min_eq_right hw.2]

Premises used: min_eq_right, max_eq_right, And.right
-- 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 : Fin 1) ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w

Tactic:
simp [hw.1, h.out.le]

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

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffOn contMDiffOn_projIcc⟩

Premises used: ContMDiff.comp_contMDiffOn, Iff.intro, contMDiffOn_projIcc
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
refine :
  ∀ (hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)),
    ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (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⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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) (M := (↑(Icc x y) : Type)) I n
    ((f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ))

Tactic:
hf.comp_contMDiff (contMDiff_subtype_coe_Icc (x := x) (y := y)) (fun z ↦ z.2)

Premises used: contMDiff_subtype_coe_Icc, ContMDiffOn.comp_contMDiff, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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)
h₁ : f = (f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f

Tactic:
convert! hf.comp_contMDiff (contMDiff_subtype_coe_Icc (x := x) (y := y)) (fun z ↦ z.2)

Premises used: contMDiff_subtype_coe_Icc, ContMDiffOn.comp_contMDiff, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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)
h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z
⊢ f = (f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)

Tactic:
ext z
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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)
z : (↑(Icc x y) : Type)
⊢ f z = ((f ∘ projIcc x y ⋯) ∘ fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) z

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 : ContMDiffAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f w
⊢ projIcc x y ⋯ (↑w : ℝ) = w

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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)
refine :
  ∀ (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
⊢ ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (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)⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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) 𝓘(ℝ, ℝ) (M' := ℝ) n
    (fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w

Tactic:
have A := contMDiff_subtype_coe_Icc (x := x) (y := y) (n := n) w
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
⊢ 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 ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) univ w

Tactic:
hf.comp _ A (fun z hz ↦ z.2)

Premises used: Subtype.property, ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
⊢ ContMDiffWithinAt (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I n f univ w

Tactic:
convert! hf.comp _ A (fun z hz ↦ z.2)

Premises used: Subtype.property, ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z
⊢ f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)

Tactic:
ext z
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
z : (↑(Icc x y) : Type)
⊢ f z = ((f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
refine_2 : ∀ (hf : MDiffAt f w), MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ) ↔ MDiffAt f w

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w

Tactic:
have A := (contMDiff_subtype_coe_Icc (x := x) (y := y) w).mdifferentiableAt one_ne_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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[univ] fun (z : (↑(Icc x y) : Type)) ↦ (↑z : ℝ)) w

Tactic:
rw [← mdifferentiableWithinAt_univ] at A ⊢

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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 ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) w

Tactic:
hf.comp _ A (fun z hz ↦ z.2)

Premises used: MDifferentiableWithinAt.comp, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
⊢ MDiffAt[univ] f w

Tactic:
convert! hf.comp _ A (fun z hz ↦ z.2)

Premises used: MDifferentiableWithinAt.comp, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
h₁ : ∀ (z : (↑(Icc x y) : Type)), f z = ((f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z
⊢ f = (f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)

Tactic:
ext z
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
z : (↑(Icc x y) : Type)
⊢ f z = ((f ∘ projIcc x y ⋯) ∘ Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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] (projIcc x y ⋯) (↑w : ℝ)

Tactic:
have := (contMDiffOn_projIcc (x := x) (y := y) w w.2).mdifferentiableWithinAt one_ne_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
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
this : MDiffAt[Icc x y] (projIcc x y ⋯) (↑w : ℝ)
⊢ projIcc x y ⋯ (↑w : ℝ) = w

Tactic:
simp