awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (IccLeftChart x y).symm.symm.target
hz₂ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (↑(IccLeftChart x y).symm.symm.symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ⁻¹' (IccRightChart x y).source
hz₃ : z.ofLp 0 + x < y
⊢ x < min (z.ofLp 0 + x) y

Tactic:
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, update_self,
      max_eq_left, hz₀, lt_sub_iff_add_lt, mfld_simps] at hz₁ hz₂

Premises used: IccRightChart, max_eq_left, modelWithCornersEuclideanHalfSpace, IccLeftChart, Function.update_self, lt_sub_iff_add_lt
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : x < min (z.ofLp 0 + x) y
⊢ 0 < z.ofLp 0

Tactic:
rw [min_eq_left hz₁.le, lt_add_iff_pos_left] at hz₂

Premises used: LT.lt.le, min_eq_left, lt_add_iff_pos_left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
h :
  ∀ (i : Fin 1),
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
                (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
            ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
              (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
        i =
      ofLp (p := 2)
        ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
            toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
          this)
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
        i
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
h :
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
h : y - (z.ofLp 0 + x) = -z.ofLp 0 + (y - x)
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0

Tactic:
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, *,
      max_eq_left, min_eq_left hz₁.le, update_self, mfld_simps]

Premises used: IccRightChart, LT.lt.le, max_eq_left, modelWithCornersEuclideanHalfSpace, min_eq_left, IccLeftChart, Function.update_self
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ y - (z.ofLp 0 + x) = -z.ofLp 0 + (y - x)

Tactic:
abel
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
h :
  ∀
    x_2 ∈
      (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
          ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩
        range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)),
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
            (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
        x_2 =
      (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        x_2
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))

Tactic:
apply M.contDiffOn.congr

Premises used: ContDiffOn.congr, ContDiff.contDiffOn
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (IccRightChart x y).symm.symm.target
hz₂ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (↑(IccRightChart x y).symm.symm.symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ⁻¹' (IccLeftChart x y).source
⊢ z.ofLp 0 < y - x

Tactic:
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff,
      update_self, max_eq_left hz₀, mfld_simps] at hz₁ hz₂

Premises used: IccRightChart, max_lt_iff, max_eq_left, modelWithCornersEuclideanHalfSpace, IccLeftChart, Function.update_self
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (IccRightChart x y).symm.symm.target
hz₂ :
  (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) ∈
    (↑(IccRightChart x y).symm.symm.symm : EuclideanHalfSpace 1 → (↑(Icc x y) : Type)) ⁻¹' (IccLeftChart x y).source
hz₃ : z.ofLp 0 < y - x
⊢ y - z.ofLp 0 < y ∧ x < y

Tactic:
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff,
      update_self, max_eq_left hz₀, mfld_simps] at hz₁ hz₂

Premises used: IccRightChart, max_lt_iff, max_eq_left, modelWithCornersEuclideanHalfSpace, IccLeftChart, Function.update_self
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 < y - x
hz₂ : y - z.ofLp 0 < y ∧ x < y
⊢ x < y - z.ofLp 0

Tactic:
rw [lt_sub_comm] at hz₁

Premises used: lt_sub_comm
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 < y - x
hz₂ : y - z.ofLp 0 < y ∧ x < y
hz₃ : x < y - z.ofLp 0
⊢ y - z.ofLp 0 < y ∧ x < y

Tactic:
rw [lt_sub_comm] at hz₁

Premises used: lt_sub_comm
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
h :
  ∀ (i : Fin 1),
    (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
              (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
                (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
            ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
              (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
        i =
      ofLp (p := 2)
        ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
            toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
          this)
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
        i
⊢ ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
        (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
          (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)) =
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
        toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
      this)
      ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
h :
  (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      i =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      i

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
h : y - z.ofLp 0 - x = -z.ofLp 0 + (y - x)
⊢ (((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
            (↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
              (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
          ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
            (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀))).ofLp
      0 =
    ofLp (p := 2)
      ((have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
          toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
        this)
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
          (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz₀)))
      0

Tactic:
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart,
      update_self, max_eq_left, hz₀, hz₁.le, mfld_simps]

Premises used: IccRightChart, LT.lt.le, max_eq_left, modelWithCornersEuclideanHalfSpace, IccLeftChart, Function.update_self
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
⊢ y - z.ofLp 0 - x = -z.ofLp 0 + (y - x)

Tactic:
abel