awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : x < (↑p : ℝ) ∧ (↑p : ℝ) < y
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 < y.ofLp 0}
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) p)

Tactic:
exact IccLeftChart_extend_interior_pos hp

Premises used: IccLeftChart_extend_interior_pos
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
h :
  ∀ (p : (↑(Icc x y) : Type)),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
⊢ Eq (α := Set (↑(Icc x y) : Type))
    (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type))
    {⊥, ⊤}

Tactic:
ext p
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
h :
  ∀ (hp : (↑p : ℝ) = x),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
h₁ :
  ∀ (hp : (↑p : ℝ) = y),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
h₂ :
  ∀ (hp : (↑p : ℝ) ∈ Ioo x y),
    Membership.mem (γ := Set (↑(Icc x y) : Type))
        (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
          (↑(Icc x y) : Type))
        p ↔
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p

Tactic:
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc p.2 with (hp | hp | hp)

Premises used: Set.eq_endpoints_or_mem_Ioo_of_mem_Icc, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = x
⊢ p = ⊥

Tactic:
have : p = ⊥ := SetCoe.ext hp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = x
this : p = ⊥
h :
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      ⊥ ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊥
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = x
this : p = ⊥
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      ⊥ ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊥

Tactic:
apply iff_of_true Icc_isBoundaryPoint_bot (mem_insert ⊥ {⊤})

Premises used: Icc_isBoundaryPoint_bot, Bot.bot, iff_of_true, Set.mem_insert, Top.top, Singleton.singleton
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = y
⊢ p = ⊤

Tactic:
have : p = ⊤ := SetCoe.ext hp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = y
this : p = ⊤
h :
  Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      ⊤ ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊤
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) = y
this : p = ⊤
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      ⊤ ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} ⊤

Tactic:
apply iff_of_true Icc_isBoundaryPoint_top (mem_insert_of_mem ⊥ rfl)

Premises used: Set.mem_insert_of_mem, Bot.bot, iff_of_true, rfl, Icc_isBoundaryPoint_top
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) ∈ Ioo x y
h :
  p ∉
    ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type)
h₁ : p ∉ {⊥, ⊤}
⊢ Membership.mem (γ := Set (↑(Icc x y) : Type))
      (ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
        (↑(Icc x y) : Type))
      p ↔
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {⊥, ⊤} p

Tactic:
apply iff_of_false

Premises used: iff_of_false
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : (↑p : ℝ) ∈ Ioo x y
⊢ p ∉
    ModelWithCorners.boundary (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (I := 𝓡∂ 1)
      (↑(Icc x y) : Type)

Tactic:
simpa [← mem_compl_iff, ModelWithCorners.compl_boundary] using
        Icc_isInteriorPoint_interior hp

Premises used: ModelWithCorners.compl_boundary, Icc_isInteriorPoint_interior, Set.mem_compl_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
hp : (↑⊥ : ℝ) ∈ Ioo x y
⊢ False

Tactic:
simp at hp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
hp : (↑⊤ : ℝ) ∈ Ioo x y
⊢ False

Tactic:
simp at hp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
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 {⊥, ⊤})
rw₁ rw₂ : Eq.{u_3 + 1} (α := Set (M × (↑(Icc x y) : Type))) (prod univ {⊥, ⊤}) (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 {⊥, ⊤})

Tactic:
rw [I.boundary_of_boundaryless_left, boundary_Icc]

Premises used: ModelWithCorners.boundary_of_boundaryless_left, boundary_Icc
-- 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 : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
⊢ 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
-- 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 :
  ∀ (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)))
⊢ IsManifold (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) n (↑(Icc x y) : Type)

Tactic:
apply isManifold_of_contDiffOn

Premises used: isManifold_of_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)
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)))
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)))
⊢ 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:
rcases he with (rfl | rfl)

Premises used: rfl
-- 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)
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)))
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)))
⊢ 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)

Premises used: rfl
-- 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)
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)))
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)))
⊢ 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)

Premises used: rfl
-- 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)
⊢ 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:
(mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1

Premises used: Iff.mpr, ContDiffOn, symm_trans_mem_contDiffGroupoid, And.left, mem_groupoid_of_pregroupoid
-- 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)
⊢ 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:
exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1

Premises used: Iff.mpr, symm_trans_mem_contDiffGroupoid, And.left, mem_groupoid_of_pregroupoid
-- 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) ⁻¹'
          ((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
⊢ 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:
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₀)) ∈
    (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
⊢ 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