awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
hs :
  Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))

Tactic:
apply Convex.convex_isRCLikeNormedField

Premises used: Convex.convex_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))

Tactic:
rw [range_euclideanHalfSpace n]

Premises used: range_euclideanHalfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
EuclideanHalfSpace.convex (n := n)

Premises used: EuclideanHalfSpace.convex
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
exact EuclideanHalfSpace.convex (n := n)

Premises used: EuclideanHalfSpace.convex
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
rw : Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | 0 < y.ofLp 0}
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n))
    (interior
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0))))

Tactic:
rw [range_euclideanHalfSpace, interior_halfSpace]

Premises used: interior_halfSpace, range_euclideanHalfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | 0 < y.ofLp 0}
    (toLp 2 fun (i : Fin n) ↦ 1)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | 0 < y.ofLp 0}

Tactic:
exact ⟨toLp 2 fun i ↦ 1, by simp⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Continuous (Y := EuclideanHalfSpace n) fun (x : EuclideanSpace ℝ (Fin n)) ↦
    Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2 (update (β := fun (x : Fin n) ↦ ℝ) x.ofLp 0 (max (x.ofLp 0) 0))) ⋯

Tactic:
((PiLp.continuous_toLp 2 _).comp <| (PiLp.continuous_ofLp 2 _).update 0 <|
      (PiLp.continuous_apply 2 _ 0).max continuous_const).subtype_mk _

Premises used: PiLp.continuous_toLp, Continuous.comp, EuclideanHalfSpace, continuous_const, Continuous.subtype_mk, Continuous.update, PiLp.continuous_apply, PiLp.continuous_ofLp, Continuous.max, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Continuous (Y := EuclideanHalfSpace n) fun (x : EuclideanSpace ℝ (Fin n)) ↦
    Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2 (update (β := fun (x : Fin n) ↦ ℝ) x.ofLp 0 (max (x.ofLp 0) 0))) ⋯

Tactic:
exact ((PiLp.continuous_toLp 2 _).comp <| (PiLp.continuous_ofLp 2 _).update 0 <|
      (PiLp.continuous_apply 2 _ 0).max continuous_const).subtype_mk _

Premises used: PiLp.continuous_toLp, Continuous.comp, continuous_const, Continuous.subtype_mk, Continuous.update, PiLp.continuous_apply, PiLp.continuous_ofLp, Continuous.max, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
i : Fin n
⊢ LE.le (α := (fun (x : Fin n) ↦ ℝ) i) 0 (ofLp (p := 2) (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) i)

Tactic:
simp only [le_sup_right]

Premises used: le_sup_right
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanQuadrant n
h_1 : Membership.mem (γ := Set (EuclideanQuadrant n)) univ x
h :
  ∀ (i : Fin n),
    ofLp (p := 2)
        (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
              (toLp 2 fun (i : Fin n) ↦ max ((↑x : EuclideanSpace ℝ (Fin n)).ofLp i) 0) ⋯) :
          EuclideanSpace ℝ (Fin n))
        i =
      (↑x : EuclideanSpace ℝ (Fin n)).ofLp i
⊢ Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
      (toLp 2 fun (i : Fin n) ↦ max ((↑x : EuclideanSpace ℝ (Fin n)).ofLp i) 0) ⋯ =
    x

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanQuadrant n
h : Membership.mem (γ := Set (EuclideanQuadrant n)) univ x
i : Fin n
⊢ ofLp (p := 2)
      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
            (toLp 2 fun (i : Fin n) ↦ max ((↑x : EuclideanSpace ℝ (Fin n)).ofLp i) 0) ⋯) :
        EuclideanSpace ℝ (Fin n))
      i =
    (↑x : EuclideanSpace ℝ (Fin n)).ofLp i

Tactic:
simp only [x.2 i, sup_of_le_left]

Premises used: sup_of_le_left, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x
h :
  ∀ (i : Fin n),
    ofLp (p := 2)
        (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
              (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) ⋯) :
          EuclideanSpace ℝ (Fin n))
        i =
      x.ofLp i
⊢ (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
          (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) ⋯) :
      EuclideanSpace ℝ (Fin n)) =
    x

Tactic:
ext1 i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x
i : Fin n
⊢ ofLp (p := 2)
      (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)
            (toLp 2 fun (i : Fin n) ↦ max (x.ofLp i) 0) ⋯) :
        EuclideanSpace ℝ (Fin n))
      i =
    x.ofLp i

Tactic:
simp only [hx i, sup_of_le_left]

Premises used: sup_of_le_left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
simp :
  Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
⊢ if h : IsRCLikeNormedField ℝ then
    Convex ℝ (E := EuclideanSpace ℝ (Fin n))
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
  else
    Eq (α := Set (EuclideanSpace ℝ (Fin n)))
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
      univ

Tactic:
simp only [instIsRCLikeNormedField, ↓reduceDIte]

Premises used: reduceDIte, instIsRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
hs :
  Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))

Tactic:
apply Convex.convex_isRCLikeNormedField

Premises used: Convex.convex_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
hs : Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanQuadrant n)
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))

Tactic:
rw [range_euclideanQuadrant]

Premises used: range_euclideanQuadrant
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}

Tactic:
EuclideanQuadrant.convex

Premises used: setOf, EuclideanQuadrant.convex
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Convex ℝ (E := EuclideanSpace ℝ (Fin n)) {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}

Tactic:
exact EuclideanQuadrant.convex

Premises used: EuclideanQuadrant.convex
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
rw : Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), 0 < y.ofLp i}
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n))
    (interior
      (range (ι := EuclideanQuadrant n)
        (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i))))

Tactic:
rw [range_euclideanQuadrant, interior_euclideanQuadrant]

Premises used: range_euclideanQuadrant, interior_euclideanQuadrant
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), 0 < y.ofLp i}
    (toLp 2 fun (i : Fin n) ↦ 1)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Set.Nonempty (α := EuclideanSpace ℝ (Fin n)) {y : PiLp 2 fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), 0 < y.ofLp i}

Tactic:
exact ⟨toLp 2 fun i ↦ 1, by simp⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) 0 = 0

Tactic:
rfl

Premises used: ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
    {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
range_euclideanHalfSpace n

Premises used: EuclideanHalfSpace, ModelWithCorners.toFun', range_euclideanHalfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
h :
  range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
    {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
⊢ interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    interior {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
congr!
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
    {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
apply range_euclideanHalfSpace

Premises used: range_euclideanHalfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n))) (interior {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0})
    {y : EuclideanSpace ℝ (Fin n) | 0 < y.ofLp 0}

Tactic:
interior_halfSpace _ _ _

Premises used: setOf, interior_halfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
calc :
  interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    interior {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
⊢ interior (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    {y : EuclideanSpace ℝ (Fin n) | 0 < y.ofLp 0}

Tactic:
calc interior (range (𝓡∂ n))
    _ = interior ({ y | 0 ≤ y 0}) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 < y 0 } := interior_halfSpace _ _ _

Premises used: setOf, interior_halfSpace, ModelWithCorners.toFun', LE.le, modelWithCornersEuclideanHalfSpace, interior, Set.range, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
h :
  range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n)) =
    {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
⊢ frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    frontier {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
congr!
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n))) (frontier {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0})
    {y : EuclideanSpace ℝ (Fin n) | 0 = y.ofLp 0}

Tactic:
frontier_halfSpace 2 _ _

Premises used: frontier_halfSpace, setOf, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
calc :
  frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    frontier {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}
⊢ frontier (range (ι := EuclideanHalfSpace n) (↑(𝓡∂ n) : EuclideanHalfSpace n → EuclideanSpace ℝ (Fin n))) =
    {y : EuclideanSpace ℝ (Fin n) | 0 = y.ofLp 0}

Tactic:
calc frontier (range (𝓡∂ n))
    _ = frontier ({ y | 0 ≤ y 0 }) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 = y 0 } := frontier_halfSpace 2 _ _

Premises used: frontier, frontier_halfSpace, setOf, ModelWithCorners.toFun', LE.le, modelWithCornersEuclideanHalfSpace, Set.range, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
⊢ min ((↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x) y ∈ Icc x y

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

Premises used: LT.lt.le, Subtype.prop, Fact.out
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : (↑(Icc x y) : Type)⦄,
    Membership.mem (γ := Set (↑(Icc x y) : Type)) {z : (↑(Icc x y) : Type) | (↑z : ℝ) < y} x_1 →
      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_2 : Fin 1) ↦ (↑x_1 : ℝ) - x)
          ⋯)

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

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

Tactic:
simp only [min_lt_iff, mem_setOf_eq]

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

Tactic:
left
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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
⊢ (↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x < y

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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) | (↑z : ℝ) < y}
    (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ 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 y : ℝ
h : Fact (x < y)
z : ℝ
hz_1 : z ∈ Icc x y
h'z : z < y
hz : x ≤ z ∧ z ≤ y
⊢ Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y)
      (min
        (ofLp (p := 2)
            (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
                  (toLp 2 fun (x_1 : Fin 1) ↦ (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y) z hz_1) : ℝ) - x) ⋯) :
              EuclideanSpace ℝ (Fin 1))
            0 +
          x)
        y)
      ⋯ =
    Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) z hz_1

Tactic:
simp only [Fin.isValue, sub_add_cancel, hz, inf_of_le_left]

Premises used: inf_of_le_left, Fin.isValue, sub_add_cancel
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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_1 : Fin 1) ↦
      (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
              (min
                ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0 +
                  x)
                y)
              ⋯) :
          ℝ) -
        x) =
    z
⊢ Eq (α := EuclideanHalfSpace 1)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2 fun (x_1 : Fin 1) ↦
        (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                (min
                  ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                          EuclideanSpace ℝ (Fin 1)).ofLp
                      0 +
                    x)
                  y)
                ⋯) :
            ℝ) -
          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 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_1 : Fin 1) ↦
          (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
                  (min
                    ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                            EuclideanSpace ℝ (Fin 1)).ofLp
                        0 +
                      x)
                    y)
                  ⋯) :
              ℝ) -
            x)
        i =
      z.ofLp i
⊢ (toLp 2 fun (x_1 : Fin 1) ↦
      (↑(Subtype.mk (p := fun (x_2 : ℝ) ↦ x_2 ∈ Icc x y)
              (min
                ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin 1)) ↦ 0 ≤ x.ofLp 0) z hz) :
                        EuclideanSpace ℝ (Fin 1)).ofLp
                    0 +
                  x)
                y)
              ⋯) :
          ℝ) -
        x) =
    z

Tactic:
ext i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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 < x + z.ofLp 0 → z.ofLp 0 - (y - x) + (y - (x + z.ofLp 0)) = 0
⊢ x + z.ofLp 0 ≤ y

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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 + z.ofLp 0 ≤ y

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

Tactic:
simp only [Fin.isValue, add_comm, A, inf_of_le_left, add_sub_cancel_left]

Premises used: inf_of_le_left, add_sub_cancel_left, add_comm, Fin.isValue
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
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 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 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 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 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_1 : Fin 1) ↦ (↑z : ℝ) - x) ⋯)
    {z : (↑(Icc x y) : Type) | (↑z : ℝ) < y}

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn (Y := (↑(Icc x y) : Type))
    (fun (z : EuclideanHalfSpace 1) ↦
      Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc x y) (min ((↑z : EuclideanSpace ℝ (Fin 1)).ofLp 0 + x) y) ⋯)
    {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)
⊢ Fact (x ≤ y)

Tactic:
Fact.mk hxy.out.le

Premises used: LT.lt.le, Fact.mk, Fact.out