awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
norm_num :
  Eq (α := EuclideanSpace ℝ (Fin 1))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x : Fin 1) ↦ 0) ⋯))
    0
⊢ (↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥ = 0

Tactic:
norm_num [IccLeftChart, modelWithCornersEuclideanHalfSpace_zero]

Premises used: modelWithCornersEuclideanHalfSpace_zero, IccLeftChart
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Eq (α := EuclideanSpace ℝ (Fin 1))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x : Fin 1) ↦ 0) ⋯))
    0

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
⊢ ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) p).ofLp 0 = (↑p : ℝ) - x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : x < (↑p : ℝ) ∧ (↑p : ℝ) < y
⊢ 0 < (↑p : ℝ) - x

Tactic:
norm_num [hp.1]

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
rw₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 = y.ofLp 0} 0
rw₂ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 (ofLp (p := 2) 0 0)
rw₃ rw₄ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 0
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)

Tactic:
rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]

Premises used: frontier_range_modelWithCornersEuclideanHalfSpace, Set.mem_setOf, IccLeftChart_extend_bot, PiLp.zero_apply
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
⊢ max (y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0) x ∈ Icc x y

Tactic:
simp [z.prop, h.out.le, sub_eq_add_neg]

Premises used: sub_eq_add_neg, LT.lt.le, Subtype.prop, Fact.out
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_2 : (↑(Icc x y) : Type)⦄,
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | x < (↑z : ℝ)} x_2 →
      Membership.mem (γ := Set (EuclideanHalfSpace 1))
        {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
        (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x_3 : Fin 1) ↦ y - (↑x_2 : ℝ))
          ⋯)

Tactic:
simp only [mem_setOf_eq, Fin.isValue, sub_lt_sub_iff_left,
    imp_self, implies_true]

Premises used: Set.mem_setOf_eq, Fin.isValue, imp_self, sub_lt_sub_iff_left, implies_true
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
simp :
  ∀ ⦃x_2 : EuclideanHalfSpace 1⦄,
    (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x → x < y - (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0 ∨ x < x
⊢ ∀ ⦃x_2 : EuclideanHalfSpace 1⦄,
    Membership.mem (γ := Set (EuclideanHalfSpace 1))
        {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x} x_2 →
      Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | x < (↑z : ℝ)}
        (Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y) (max (y - (↑x_2 : EuclideanSpace ℝ (Fin 1)).ofLp 0) x) ⋯)

Tactic:
simp only [lt_max_iff, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, lt_max_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x
h₁ : x < y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0
⊢ x < y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 ∨ x < x

Tactic:
left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x
linarith :
  y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 ≤ x →
    (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 - (y - x) + (y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 - x) = 0
⊢ x < y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z :
  Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | x < (↑z : ℝ)}
    (Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) z hz)
⊢ x ≤ z ∧ z ≤ y

Tactic:
simp only [mem_setOf_eq, mem_Icc] at hz h'z

Premises used: Set.mem_setOf_eq, Set.mem_Icc
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : ℝ
hz_1 : z ∈ Icc x y
h'z : x < z
hz : x ≤ z ∧ z ≤ y
⊢ Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
      (max
        (y -
          ofLp (p := 2)
            (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
                  (toLp 2 fun (x_2 : Fin 1) ↦ y - (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y) z hz_1) : ℝ)) ⋯) :
              EuclideanSpace ℝ (Fin 1))
            0)
        x)
      ⋯ =
    Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) z hz_1

Tactic:
simp only [Fin.isValue, sub_eq_add_neg, neg_add_rev, neg_neg,
      add_neg_cancel_comm_assoc, hz, sup_of_le_left]

Premises used: neg_add_rev, sub_eq_add_neg, neg_neg, Fin.isValue, add_neg_cancel_comm_assoc, sup_of_le_left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z :
  Membership.mem (γ := Set (EuclideanHalfSpace 1))
    {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
rw :
  (toLp 2 fun (x_2 : Fin 1) ↦
      y -
        (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
              (max
                (y -
                  (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0)
                x)
              ⋯) :
          ℝ)) =
    z
⊢ Eq (α := EuclideanHalfSpace 1)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      ⋯)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)

Tactic:
rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z :
  Membership.mem (γ := Set (EuclideanHalfSpace 1))
    {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz)
h₁ :
  ∀ (i : Fin 1),
    ofLp (p := 2)
        (toLp 2 fun (x_2 : Fin 1) ↦
          y -
            (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                  (max
                    (y -
                      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                            EuclideanSpace ℝ (Fin 1)).ofLp
                        0)
                    x)
                  ⋯) :
              ℝ))
        i =
      z.ofLp i
⊢ (toLp 2 fun (x_2 : Fin 1) ↦
      y -
        (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
              (max
                (y -
                  (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0)
                x)
              ⋯) :
          ℝ)) =
    z

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
linarith : y - z.ofLp 0 < x → z.ofLp 0 - (y - x) + (y - z.ofLp 0 - x) = 0
⊢ x ≤ y - z.ofLp 0

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
⊢ x ≤ y - z.ofLp 0

Tactic:
have A : x ≤ y - z 0 := by linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
h₁ :
  ofLp (p := 2)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      0 =
    z.ofLp 0
⊢ ofLp (p := 2)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      i =
    z.ofLp 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)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ ofLp (p := 2)
      (toLp 2 fun (x_2 : Fin 1) ↦
        y -
          (↑(Subtype.mk (p := fun (x_3 : ℝ) ↦ x_3 ∈ Icc x y)
                (max
                  (y -
                    (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0)
                  x)
                ⋯) :
            ℝ))
      0 =
    z.ofLp 0

Tactic:
simp only [Fin.isValue, A, sup_of_le_left, sub_sub_cancel]

Premises used: sub_sub_cancel, Fin.isValue, sup_of_le_left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
⊢ IsOpen (X := ℝ) {z : ℝ | z < y - x}

Tactic:
have : IsOpen { z : ℝ | z < y - x } := isOpen_Iio
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
this : IsOpen (X := ℝ) {z : ℝ | z < y - x}
⊢ IsOpen (X := EuclideanSpace ℝ (Fin 1)) {z : EuclideanSpace ℝ (Fin 1) | z.ofLp 0 < y - x}

Tactic:
have : IsOpen { z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x } :=
      this.preimage (@PiLp.continuous_apply 2 (Fin 1) (fun _ ↦ ℝ) _ 0)
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
this_1 : IsOpen (X := ℝ) {z : ℝ | z < y - x}
this : IsOpen (X := EuclideanSpace ℝ (Fin 1)) {z : EuclideanSpace ℝ (Fin 1) | z.ofLp 0 < y - x}
⊢ IsOpen (X := EuclideanHalfSpace 1) {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}

Tactic:
this.preimage continuous_subtype_val

Premises used: continuous_subtype_val, Set.Mem, EuclideanHalfSpace, setOf, Set.preimage, IsOpen.preimage
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
this_1 : IsOpen (X := ℝ) {z : ℝ | z < y - x}
this : IsOpen (X := EuclideanSpace ℝ (Fin 1)) {z : EuclideanSpace ℝ (Fin 1) | z.ofLp 0 < y - x}
⊢ IsOpen (X := EuclideanHalfSpace 1) {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}

Tactic:
exact this.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn (Y := EuclideanHalfSpace 1)
    (fun (z : (↑(Icc x y) : Type)) ↦
      Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x_2 : Fin 1) ↦ y - (↑z : ℝ)) ⋯)
    {z : (↑(Icc x y) : Type) | x < (↑z : ℝ)}

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn (Y := (↑(Icc x y) : Type))
    (fun (z : EuclideanHalfSpace 1) ↦
      Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) (max (y - (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0) x) ⋯)
    {z : EuclideanHalfSpace 1 | (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 < y - x}

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
norm_num :
  Eq (α := EuclideanSpace ℝ (Fin 1))
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))
      (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) (toLp 2 fun (x : Fin 1) ↦ 0) ⋯))
    0
⊢ (↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤ = 0

Tactic:
norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero]

Premises used: IccRightChart, modelWithCornersEuclideanHalfSpace_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))) 0
rw₁ : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1))) {y : EuclideanSpace ℝ (Fin 1) | 0 = y.ofLp 0} 0
rw₂ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 (ofLp (p := 2) 0 0)
rw₃ rw₄ : Eq (α := (fun (x : Fin 1) ↦ ℝ) 0) 0 0
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)

Tactic:
rw [IccRightChart_extend_top, frontier_range_modelWithCornersEuclideanHalfSpace,
    mem_setOf, PiLp.zero_apply]

Premises used: frontier_range_modelWithCornersEuclideanHalfSpace, Set.mem_setOf, PiLp.zero_apply, IccRightChart_extend_top
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
pos : ∀ (h' : (↑z : ℝ) < y), z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
neg : ∀ (h' : ¬(↑z : ℝ) < y), z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
by_cases h' : z.val < y

Premises used: Subtype.val
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : (↑z : ℝ) < y
pos : z ∈ (IccLeftChart x y).source
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
simp only [h', if_true]

Premises used: if_true
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : (↑z : ℝ) < y
⊢ z ∈ (IccLeftChart x y).source

Tactic:
h'

Premises used: Set.Mem, setOf
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : (↑z : ℝ) < y
⊢ z ∈ (IccLeftChart x y).source

Tactic:
exact h'
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
neg : z ∈ (IccRightChart x y).source
⊢ z ∈ (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
simp only [h', if_false]

Premises used: if_false
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
neg : y ≤ (↑z : ℝ)
⊢ z ∈ (IccRightChart x y).source

Tactic:
apply lt_of_lt_of_le h.out

Premises used: Fact.out, lt_of_lt_of_le
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
⊢ y ≤ (↑z : ℝ)

Tactic:
simpa only [not_lt] using h'

Premises used: not_lt
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
pos :
  ∀ (h' : (↑z : ℝ) < y),
    Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
      {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
neg :
  ∀ (h' : ¬(↑z : ℝ) < y),
    Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
      {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)

Tactic:
by_cases h' : (z : ℝ) < y

Premises used: Subtype.val
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : (↑z : ℝ) < y
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)

Tactic:
simp [h']
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
x y : ℝ
h : Fact (x < y)
z : (↑(Icc x y) : Type)
h' : ¬(↑z : ℝ) < y
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (↑(Icc x y) : Type) (EuclideanHalfSpace 1)))
    {IccLeftChart x y, IccRightChart x y} (if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y)

Tactic:
simp [h']
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
z : (↑(Icc x y) : Type)
⊢ chartAt (EuclideanHalfSpace 1) z = if (↑z : ℝ) < y then IccLeftChart x y else IccRightChart x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
z : (↑(Icc x y) : Type)
h : (↑z : ℝ) < y
⊢ chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y

Tactic:
simp [Icc_chartedSpaceChartAt, h]

Premises used: Icc_chartedSpaceChartAt
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
z : (↑(Icc x y) : Type)
h : y ≤ (↑z : ℝ)
⊢ chartAt (EuclideanHalfSpace 1) z = IccRightChart x y

Tactic:
simp [Icc_chartedSpaceChartAt, reduceIte, not_lt.mpr h]

Premises used: Iff.mpr, Icc_chartedSpaceChartAt, not_lt, reduceIte
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ (↑⊥ : ℝ) < y

Tactic:
simp [hxy.out]

Premises used: Fact.out
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)
⊢ ModelWithCorners.IsBoundaryPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M :=
    (↑(Icc x y) : Type)) ⊥

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])]

Premises used: extChartAt, Icc_chartedSpaceChartAt_of_le_top, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)

Tactic:
IccLeftChart_extend_bot_mem_frontier

Premises used: Set.Mem, IccLeftChart_extend_bot_mem_frontier
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccLeftChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊥)

Tactic:
exact IccLeftChart_extend_bot_mem_frontier

Premises used: IccLeftChart_extend_bot_mem_frontier
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ y ≤ (↑⊤ : ℝ)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
rw :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)
⊢ ModelWithCorners.IsBoundaryPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M :=
    (↑(Icc x y) : Type)) ⊤

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    Icc_chartedSpaceChartAt_of_top_le (by simp)]

Premises used: extChartAt, Icc_chartedSpaceChartAt_of_top_le, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)

Tactic:
IccRightChart_extend_top_mem_frontier

Premises used: Set.Mem, IccRightChart_extend_top_mem_frontier
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin 1)))
    (frontier (range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1))))
    ((↑((IccRightChart x y).extend (𝓡∂ 1)) : (↑(Icc x y) : Type) → EuclideanSpace ℝ (Fin 1)) ⊤)

Tactic:
exact IccRightChart_extend_top_mem_frontier

Premises used: IccRightChart_extend_top_mem_frontier
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
p : (↑(Icc x y) : Type)
hp : x < (↑p : ℝ) ∧ (↑p : ℝ) < y
rw :
  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)
⊢ ModelWithCorners.IsInteriorPoint (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) p

Tactic:
rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
    interior_range_modelWithCornersEuclideanHalfSpace]

Premises used: extChartAt, ModelWithCorners.IsInteriorPoint, Icc_chartedSpaceChartAt_of_le_top, And.right, interior_range_modelWithCornersEuclideanHalfSpace
-- 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:
IccLeftChart_extend_interior_pos hp

Premises used: Set.Mem, IccLeftChart_extend_interior_pos, setOf