awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n_1 n : ℕ
inst : NeZero n
⊢ LE.le (α := (fun (x : Fin n) ↦ ℝ) 0) 0 (ofLp (p := 2) 0 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n_1 n : ℕ
⊢ ∀ (i : Fin n), LE.le (α := (fun (x : Fin n) ↦ ℝ) i) 0 (ofLp (p := 2) 0 i)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x y : EuclideanQuadrant n
h : (↑x : EuclideanSpace ℝ (Fin n)) = (↑y : EuclideanSpace ℝ (Fin n))
⊢ x = y

Tactic:
Subtype.ext h

Premises used: EuclideanQuadrant, Subtype.ext
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x y : EuclideanHalfSpace n
h : (↑x : EuclideanSpace ℝ (Fin n)) = (↑y : EuclideanSpace ℝ (Fin n))
⊢ x = y

Tactic:
Subtype.ext h

Premises used: EuclideanHalfSpace, Subtype.ext
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
x_1 : EuclideanSpace ℝ (Fin n)
hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x_1
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
dsimp : 0 ≤ x_2 * x.ofLp 0 + x_3 * x_1.ofLp 0
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0}
    (x_2 • x + x_3 • x_1)

Tactic:
dsimp at hx hy ⊢
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : 0 ≤ x.ofLp 0
x_1 : EuclideanSpace ℝ (Fin n)
hy : 0 ≤ x_1.ofLp 0
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
⊢ 0 ≤ x_2 * x.ofLp 0 + x_3 * x_1.ofLp 0

Tactic:
positivity
-- 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
x_1 : EuclideanSpace ℝ (Fin n)
hy :
  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} x_1
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
dsimp : 0 ≤ x_2 * x.ofLp i + x_3 * x_1.ofLp i
⊢ 0 ≤ (x_2 • x + x_3 • x_1).ofLp i

Tactic:
dsimp at hx hy ⊢
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : ∀ (i : Fin n), 0 ≤ x.ofLp i
x_1 : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x_1.ofLp i
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
⊢ 0 ≤ x.ofLp i

Tactic:
specialize hx i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x x_1 : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x_1.ofLp i
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
hx : 0 ≤ x.ofLp i
⊢ 0 ≤ x_1.ofLp i

Tactic:
specialize hy i
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
x x_1 : EuclideanSpace ℝ (Fin n)
x_2 x_3 : ℝ
h : 0 ≤ x_2
h_1 : 0 ≤ x_3
h_2 : x_2 + x_3 = 1
i : Fin n
hx : 0 ≤ x.ofLp i
hy : 0 ≤ x_1.ofLp i
⊢ 0 ≤ x_2 * x.ofLp i + x_3 * x_1.ofLp i

Tactic:
positivity
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ LocPathConnectedSpace (EuclideanHalfSpace n)

Tactic:
EuclideanHalfSpace.convex.locPathConnectedSpace

Premises used: Set.Mem, EuclideanHalfSpace, EuclideanHalfSpace.convex, Convex.locPathConnectedSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ LocPathConnectedSpace (EuclideanQuadrant n)

Tactic:
EuclideanQuadrant.convex.locPathConnectedSpace

Premises used: Set.Mem, setOf, EuclideanQuadrant.convex, Convex.locPathConnectedSpace, EuclideanQuadrant
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    (range (ι := { x : EuclideanSpace ℝ (Fin n) // 0 ≤ x.ofLp 0 })
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
    {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

Tactic:
Subtype.range_val

Premises used: Set.Mem, Subtype.range_val
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
change : interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i}

Tactic:
change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a

Premises used: Set.Ioi, Set.Ici, Set.preimage, interior
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
hf₂ : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
⊢ interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_interior_eq_interior_preimage, interior_Ici]

Premises used: interior_Ici, IsOpenMap.preimage_interior_eq_interior_preimage, PiLp.isOpenMap_apply
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
change : closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (closure {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i}

Tactic:
change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a

Premises used: Set.Ici, closure, Set.preimage
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
hfc : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
⊢ closure (f ⁻¹' Ici a) = f ⁻¹' Ici a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ici]

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage, PiLp.isOpenMap_apply, closure_Ici
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
change : closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (closure {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i}

Tactic:
change closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a

Premises used: Set.Ioi, Set.Ici, closure, Set.preimage
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
hfc : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
⊢ closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ioi]

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage, PiLp.isOpenMap_apply, closure_Ioi
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
rw :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ))
    ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (frontier {y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}

Tactic:
rw [frontier, closure_halfSpace, interior_halfSpace]

Premises used: frontier, interior_halfSpace, closure_halfSpace
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
h :
  ∀ (y : PiLp p fun (x : Fin n) ↦ ℝ),
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ))
        ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i}) y ↔
      Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i} y
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ))
    ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i}

Tactic:
ext y
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
y : PiLp p fun (x : Fin n) ↦ ℝ
⊢ Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ))
      ({y : PiLp p fun (x : Fin n) ↦ ℝ | a ≤ y.ofLp i} \ {y : PiLp p fun (x : Fin n) ↦ ℝ | a < y.ofLp i}) y ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | a = y.ofLp i} y

Tactic:
simpa only [mem_diff, mem_setOf_eq, not_lt] using antisymm_iff

Premises used: antisymm_iff, Set.mem_setOf_eq, not_lt, Set.mem_diff
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    (range (ι := { x : EuclideanSpace ℝ (Fin n) // ∀ (i : Fin n), 0 ≤ x.ofLp i })
      (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ ∀ (i : Fin n), 0 ≤ x.ofLp i)))
    {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}

Tactic:
Subtype.range_val

Premises used: Set.Mem, setOf, Subtype.range_val
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  ∀ (x : PiLp p fun (x : Fin n) ↦ ℝ),
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ))
        {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i} x ↔
      Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ici a) x
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
x : PiLp p fun (x : Fin n) ↦ ℝ
h : (∀ (i : Fin n), a ≤ x.ofLp i) ↔ ∀ (i : Fin n), a ≤ f i x
⊢ Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ici a) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
x : PiLp p fun (x : Fin n) ↦ ℝ
⊢ (∀ (i : Fin n), a ≤ x.ofLp i) ↔ ∀ (i : Fin n), a ≤ f i x

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)

Tactic:
have h : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a ≤ y i } = ⋂ i, (f i) ⁻¹' Ici a := by
    ext; simp; rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h₁ :
  ∀ (x : PiLp p fun (x : Fin n) ↦ ℝ),
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ))
        {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i} x ↔
      Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ioi a) x
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
x : PiLp p fun (x : Fin n) ↦ ℝ
h₁ : (∀ (i : Fin n), a < x.ofLp i) ↔ ∀ (i : Fin n), a < f i x
⊢ Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
      x ↔
    Membership.mem (γ := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), f i ⁻¹' Ioi a) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
x : PiLp p fun (x : Fin n) ↦ ℝ
⊢ (∀ (i : Fin n), a < x.ofLp i) ↔ ∀ (i : Fin n), a < f i x

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)

Tactic:
have h' : { y : PiLp p (fun _ : Fin n ↦ ℝ) | ∀ i : Fin n, a < y i } = ⋂ i, (f i) ⁻¹' Ioi a := by
    ext; simp; rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
rw : Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), interior (f i ⁻¹' Ici a)) (⋂ (i : Fin n), f i ⁻¹' Ioi a)
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (interior {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i})
    {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}

Tactic:
rw [h, h', interior_iInter_of_finite]

Premises used: interior_iInter_of_finite
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
apply : ∀ (i : Fin n), interior (f i ⁻¹' Ici a) = f i ⁻¹' Ioi a
⊢ Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) (⋂ (i : Fin n), interior (f i ⁻¹' Ici a)) (⋂ (i : Fin n), f i ⁻¹' Ioi a)

Tactic:
apply iInter_congr fun i ↦ ?_

Premises used: Set.iInter_congr
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
i : Fin n
hf₂ : Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i
⊢ interior (f i ⁻¹' Ici a) = f i ⁻¹' Ioi a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_interior_eq_interior_preimage, interior_Ici]

Premises used: interior_Ici, IsOpenMap.preimage_interior_eq_interior_preimage, PiLp.isOpenMap_apply
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : (i : Fin n) → (PiLp p fun (x : Fin n) ↦ ℝ) → ℝ := fun (i : Fin n) (x : PiLp p fun (x : Fin n) ↦ ℝ) ↦ x.ofLp i
h :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a ≤ y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ici a)
h' :
  Eq (α := Set (PiLp p fun (x : Fin n) ↦ ℝ)) {y : PiLp p fun (x : Fin n) ↦ ℝ | ∀ (i : Fin n), a < y.ofLp i}
    (⋂ (i : Fin n), f i ⁻¹' Ioi a)
i : Fin n
⊢ Continuous (Y := ℝ) fun (f : PiLp p fun (x : Fin n) ↦ ℝ) ↦ f.ofLp i

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
⊢ 0 ≤ ofLp (p := 2) (toLp 2 (update (β := fun (x : Fin n) ↦ ℝ) x.ofLp 0 (max (x.ofLp 0) 0))) 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
h :
  Membership.mem (γ := Set (EuclideanHalfSpace n)) univ
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)
rw :
  max
        ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          0)
        0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        xval 0 ∧
    ∀ (x : Fin n),
      x ≠ 0 →
        (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
                EuclideanSpace ℝ (Fin n)).ofLp
            x =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            xval x
⊢ Eq (α := EuclideanHalfSpace n)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)
      (toLp 2
        (update (β := fun (x : Fin n) ↦ ℝ)
          (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          0
          (max
            ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
                  EuclideanSpace ℝ (Fin n)).ofLp
              0)
            0)))
      ⋯)
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)

Tactic:
rw [Subtype.mk_eq_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]

Premises used: Function.update_eq_iff, Equiv.symm_apply_eq, WithLp.equiv_symm_apply, Subtype.mk_eq_mk
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
h :
  Membership.mem (γ := Set (EuclideanHalfSpace n)) univ
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)
⊢ max
        ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          0)
        0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        xval 0 ∧
    ∀ (x : Fin n),
      x ≠ 0 →
        (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
                EuclideanSpace ℝ (Fin n)).ofLp
            x =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            xval x

Tactic:
⟨max_eq_left xprop, fun i _ => rfl⟩

Premises used: max_eq_left, And.intro, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
h :
  Membership.mem (γ := Set (EuclideanHalfSpace n)) univ
    (Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop)
⊢ max
        ((↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
              EuclideanSpace ℝ (Fin n)).ofLp
          0)
        0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        xval 0 ∧
    ∀ (x : Fin n),
      x ≠ 0 →
        (↑(Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0) xval xprop) :
                EuclideanSpace ℝ (Fin n)).ofLp
            x =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            xval x

Tactic:
exact ⟨max_eq_left xprop, fun i _ => rfl⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
rw :
  max (x.ofLp 0) 0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        x 0 ∧
    ∀ (x_1 : Fin n),
      x_1 ≠ 0 →
        x.ofLp x_1 =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            x x_1
⊢ (↑(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))) ⋯) :
      EuclideanSpace ℝ (Fin n)) =
    x

Tactic:
rw [Subtype.coe_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]

Premises used: Subtype.coe_mk, Function.update_eq_iff, Equiv.symm_apply_eq, WithLp.equiv_symm_apply
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
⊢ max (x.ofLp 0) 0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        x 0 ∧
    ∀ (x_1 : Fin n),
      x_1 ≠ 0 →
        x.ofLp x_1 =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            x x_1

Tactic:
⟨max_eq_left hx, fun _ _ => rfl⟩

Premises used: max_eq_left, And.intro, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0} x
⊢ max (x.ofLp 0) 0 =
      (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
          (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
        x 0 ∧
    ∀ (x_1 : Fin n),
      x_1 ≠ 0 →
        x.ofLp x_1 =
          (WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i) :
              (a : EuclideanSpace ℝ (Fin n)) → (i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)
            x x_1

Tactic:
exact ⟨max_eq_left hx, fun _ _ => rfl⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
n : ℕ
inst : NeZero n
simp :
  Convex ℝ (E := EuclideanSpace ℝ (Fin n))
    (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
⊢ if h : IsRCLikeNormedField ℝ then
    Convex ℝ (E := EuclideanSpace ℝ (Fin n))
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0)))
  else
    Eq (α := Set (EuclideanSpace ℝ (Fin n)))
      (range (ι := EuclideanHalfSpace n) (Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦ 0 ≤ x.ofLp 0))) univ

Tactic:
simp only [instIsRCLikeNormedField, ↓reduceDIte]

Premises used: reduceDIte, instIsRCLikeNormedField