awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)

Tactic:
exact MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq (w : ℝ) hf this (by simp)

Premises used: Subtype.val, MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
simp :
  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)
⊢ 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))

Tactic:
simp only [oneTangentSpaceIcc]

Premises used: oneTangentSpaceIcc
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
e_a : z = (↑(projIcc x y ⋯ z) : ℝ)
⊢ 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)

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ z = (↑(projIcc x y ⋯ z) : ℝ)

Tactic:
simp [projIcc_of_mem h.out.le hz]

Premises used: LT.lt.le, Set.projIcc_of_mem, 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)
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))
neg :
  ∀ (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))

Tactic:
by_cases hw : MDiffAt f w

Premises used: MDifferentiableAt, modelWithCornersEuclideanHalfSpace, OfNat.ofNat
-- 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)
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))
neg₁ : ¬MDiffAt[Icc x y] (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))

Tactic:
rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]

Premises used: mfderivWithin_zero_of_not_mdifferentiableWithinAt, mfderiv_zero_of_not_mdifferentiableAt
-- 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)
hw : ¬MDiffAt f w
⊢ 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))

Tactic:
rfl
-- 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)
hw neg neg₁ neg₂ neg₃ : ¬MDiffAt f w
⊢ ¬MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) (↑w : ℝ)

Tactic:
rwa [mdifferentiableWithinAt_comp_projIcc_iff]

Premises used: mdifferentiableWithinAt_comp_projIcc_iff
-- 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)
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 : ℝ))
pos₂ : MDiffAt[Icc x y] (projIcc x y ⋯) (↑w : ℝ)
pos₃ : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc 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))

Tactic:
rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]

Premises used: mfderiv_comp_mfderivWithin
-- 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)
hw : MDiffAt f w
⊢ MDiffAt f (projIcc x y ⋯ (↑w : ℝ))

Tactic:
simp [hw]
-- 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)
hw : MDiffAt f w
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) (↑w : ℝ)

Tactic:
(contMDiffOn_projIcc _ w.2).mdifferentiableWithinAt one_ne_zero

Premises used: Set.Mem, ContMDiffWithinAt.mdifferentiableWithinAt, one_ne_zero, Subtype.property, 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)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) (↑w : ℝ)

Tactic:
exact (contMDiffOn_projIcc _ w.2).mdifferentiableWithinAt one_ne_zero

Premises used: ContMDiffWithinAt.mdifferentiableWithinAt, one_ne_zero, Subtype.property, 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)
f : (↑(Icc x y) : Type) → M
w : (↑(Icc x y) : Type)
hw : MDiffAt f w
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc x y) (↑w : ℝ)

Tactic:
(uniqueDiffOn_Icc h.out _ w.2).uniqueMDiffWithinAt

Premises used: uniqueDiffOn_Icc, UniqueDiffWithinAt.uniqueMDiffWithinAt, Fact.out, 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)
hw : MDiffAt f w
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc x y) (↑w : ℝ)

Tactic:
exact (uniqueDiffOn_Icc h.out _ w.2).uniqueMDiffWithinAt

Premises used: uniqueDiffOn_Icc, UniqueDiffWithinAt.uniqueMDiffWithinAt, Fact.out, 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)
hw : MDiffAt f w
rw : w = Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯
hx : (↑w : ℝ) ∈ Icc x y
rw₁ : w = Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯
hx₁ : (↑w : ℝ) ∈ Icc x y
⊢ w = projIcc x y ⋯ (↑w : ℝ)

Tactic:
rw [projIcc_of_mem]

Premises used: Set.projIcc_of_mem
-- 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)
hw : MDiffAt f w
⊢ w = projIcc x y ⋯ (↑w : ℝ)

Tactic:
have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]
-- 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)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
pos :
  Eq (α := TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯)))
    ((mfderiv% f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯) :
          (a : TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩) → TangentSpace I (f ⟨(↑w : ℝ), ⋯⟩))
        (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
              TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
                TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
                  (projIcc x y ⋯ (↑w : ℝ))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩)
          1) :
      TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc 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 : ℝ))))
    ((mfderiv% f (projIcc x y ⋯ (↑w : ℝ)) :
          (a : TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ))) → TangentSpace I (f (projIcc x y ⋯ (↑w : ℝ))))
        ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) (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))

Tactic:
rw [projIcc_of_mem _ w.2]

Premises used: Set.projIcc_of_mem, 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)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
pos :
  Eq (α :=
    TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
      (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯))
    (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
            TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ))) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩)
      1)
    1
⊢ Eq (α := TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯)))
    ((mfderiv% f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯) :
          (a : TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩) → TangentSpace I (f ⟨(↑w : ℝ), ⋯⟩))
        (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
              TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
                TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
                  (projIcc x y ⋯ (↑w : ℝ))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩)
          1) :
      TangentSpace I (f (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯)))
    ((mfderiv% f w : (a : TangentSpace (𝓡∂ 1) w) → TangentSpace I (f w)) 1 : TangentSpace I (f w))

Tactic:
congr 1
-- 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)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
⊢ Eq (α := TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ)))
      1)
    1

Tactic:
mfderivWithin_projIcc_one w.2

Premises used: mfderivWithin_projIcc_one, 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)
hw : MDiffAt f w
this : w = projIcc x y ⋯ (↑w : ℝ)
⊢ Eq (α :=
    TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1)
      (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (↑w : ℝ) ⋯))
    (((mfderivWithin 𝓘(ℝ, ℝ) (𝓡∂ 1) (projIcc x y ⋯) (Icc x y) (↑w : ℝ) :
          TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ) →L[ℝ]
            TangentSpace (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (projIcc x y ⋯ (↑w : ℝ))) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑w : ℝ)) → TangentSpace (𝓡∂ 1) ⟨(↑w : ℝ), ⋯⟩)
      1)
    1

Tactic:
convert! mfderivWithin_projIcc_one w.2

Premises used: mfderivWithin_projIcc_one, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
e_a :
  Eq (α :=
    TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ) →L[ℝ]
      TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
      (↑z : ℝ))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ))
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
apply : ∀ x_1 ∈ Icc x y, (Subtype.val (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) ∘ projIcc x y ⋯) x_1 = id x_1
⊢ Eq (α :=
    TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ) →L[ℝ]
      TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
      (↑z : ℝ))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ))

Tactic:
apply mfderivWithin_congr_of_mem _ z.2

Premises used: mfderivWithin_congr_of_mem, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z_1 : (↑(Icc x y) : Type)
z : ℝ
hz : z ∈ Icc x y
⊢ (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) z = id z

Tactic:
simp [projIcc_of_mem h.out.le hz]

Premises used: LT.lt.le, Set.projIcc_of_mem, Fact.out
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)

Tactic:
have A : mfderiv[Icc x y] (Subtype.val ∘ (projIcc x y h.out.le)) z 1
      = mfderiv[Icc x y] (@id ℝ) z 1 := by
    congr 1
    apply mfderivWithin_congr_of_mem _ z.2
    intro z hz
    simp [projIcc_of_mem h.out.le hz]
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
rw :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
    1
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderiv% (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)) z :
        (a : TangentSpace (𝓡∂ 1) z) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
      1)
    1

Tactic:
rw [← mfderivWithin_comp_projIcc_one, A]

Premises used: mfderivWithin_comp_projIcc_one
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
simp :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((fderivWithin ℝ id (Icc x y) (↑z : ℝ) : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
    1

Tactic:
simp only [id_eq, mfderivWithin_eq_fderivWithin]

Premises used: mfderivWithin_eq_fderivWithin, id_eq
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
rw :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((ContinuousLinearMap.id ℝ ℝ : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((fderivWithin ℝ id (Icc x y) (↑z : ℝ) : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1

Tactic:
rw [fderivWithin_id (uniqueDiffOn_Icc h.out _ z.2)]

Premises used: uniqueDiffOn_Icc, fderivWithin_id, Fact.out, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Icc
Goal:
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
A :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (↑z : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (Subtype.val (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) ∘ projIcc x y ⋯) (Icc x y)
          (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) ((Subtype.val ∘ projIcc x y ⋯) (↑z : ℝ)))
      1)
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) id (Icc x y) (↑z : ℝ) :
        (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (id (↑z : ℝ)))
      1)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ))
    ((ContinuousLinearMap.id ℝ ℝ : (a : TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) → TangentSpace 𝓘(ℝ, ℝ) (↑z : ℝ)) 1) 1

Tactic:
rfl