awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
Goal:
x y : ℝ
hxy : Fact (x < y)
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
inst_5 : I.Boundaryless
rw :
  Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type)))
    (prod univ
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type)))
    (prod univ {⊥, ⊤})
⊢ Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type)))
    (ModelWithCorners.boundary.{0, u_1, u_2, u_3} (𝕜 := ℝ) (E := E × EuclideanSpace ℝ (Fin 1)) (H :=
      ModelProd H (EuclideanHalfSpace 1)) (I := I.prod (𝓡∂ 1)) (M × (↑(Icc x y) : Type)))
    (prod univ {⊥, ⊤})
have rw₁ : Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type))) (prod univ {⊥, ⊤}) (prod univ {⊥, ⊤})
Tactic: rw [I.boundary_of_boundaryless_left, boundary_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
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 : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
⊢ IsManifold (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) n (↑(Icc x y) : Type)
have 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)
Tactic: have M : ContDiff ℝ n (show EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
      from fun z ↦ toLp 2 fun i ↦ -z i + (y - x)) :=
    PiLp.contDiff_toLp.comp <| PiLp.contDiff_ofLp.neg.add contDiff_const
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
⊢ IsManifold (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) n (↑(Icc x y) : Type)
have h : ∀ (e e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)),
  Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
      (atlas (EuclideanHalfSpace 1) (↑(Icc x y) : Type)) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
        (atlas (EuclideanHalfSpace 1) (↑(Icc x y) : Type)) e' →
      ContDiffOn ℝ n
        ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
          (↑(e.symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
            (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
        ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹' (e.symm ≫ₕ e').source ∩
          range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: apply isManifold_of_contDiffOn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑(e.symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹' (e.symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h : ContDiffOn ℝ n
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
    (↑((IccLeftChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
      (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
  ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
      ((IccLeftChart x y).symm ≫ₕ e').source ∩
    range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: rcases he with (rfl | rfl)
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
h :
  ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccLeftChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑(e.symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹' (e.symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h₁ : ContDiffOn ℝ n
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
    (↑((IccRightChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
      (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
  ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
      ((IccRightChart x y).symm ≫ₕ e').source ∩
    range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: rcases he with (rfl | rfl)
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccLeftChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h : ContDiffOn ℝ n
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
    (↑((IccLeftChart 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) ⁻¹'
      ((IccLeftChart x y).symm ≫ₕ IccLeftChart x y).source ∩
    range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: rcases he' with (rfl | rfl)
Cleared hypotheses: e', he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
h :
  ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccLeftChart 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) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ IccLeftChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccLeftChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h₁ : ContDiffOn ℝ n
  ((↑(𝓡∂ 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))
  ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
      ((IccLeftChart x y).symm ≫ₕ IccRightChart x y).source ∩
    range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: rcases he' with (rfl | rfl)
Cleared hypotheses: e', he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h : 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: rcases he' with (rfl | rfl)
Cleared hypotheses: e', he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
e' : OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1))) ChartedSpace.atlas e'
h :
  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)))
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ e') : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ e').source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h₁ : ContDiffOn ℝ n
  ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
    (↑((IccRightChart x y).symm ≫ₕ IccRightChart 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 ≫ₕ IccRightChart x y).source ∩
    range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
Tactic: rcases he' with (rfl | rfl)
Cleared hypotheses: e', he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (goal)
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)
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 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))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ IccRightChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))
have h : ∀
  x_2 ∈
    (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccLeftChart x y).symm ≫ₕ IccRightChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (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))
      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
Tactic: apply M.contDiffOn.congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
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
⊢ ((↑(𝓡∂ 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₀))
have hz₃ : 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₂
Cleared hypotheses: hz₁, hz₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Real (hypothesis)
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
⊢ ((↑(𝓡∂ 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₀))
have hz₄ : 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₂
Cleared hypotheses: hz₁, hz₂