awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), y i < z i

Tactic:
fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)

Premises used: Iff.mpr, le_abs_self, HSub.hSub, sub_le_comm, LT.lt.trans_le, Iff.mp, LE.le.trans, lt_sub_iff_add_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
refine : ∀ (i : ι), |x i - z i| ≤ ε
⊢ ∀ (i : ι), y i < z i

Tactic:
refine fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)

Premises used: Iff.mpr, le_abs_self, HSub.hSub, sub_le_comm, LT.lt.trans_le, Iff.mp, LE.le.trans, lt_sub_iff_add_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε

Tactic:
(hxz _).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε

Tactic:
exact (hxz _).le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), y i < z i

Tactic:
have hyz : ∀ i, y i < z i := by
    refine fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)
    rw [← Real.norm_eq_abs, ← dist_eq_norm]
    exact (hxz _).le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz : ∀ (i : ι), y i < z i
intro : ∀ (δ : ℝ) (hδ : 0 < δ) (hyz : ∀ (i : ι), y i + δ < z i), y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz

Premises used: Pi.exists_forall_pos_add_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
⊢ y ∈ interior s

Tactic:
mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩

Premises used: Iff.mpr, Metric.mem_ball_self, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, mem_interior
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
intro : ball y δ ⊆ s
⊢ y ∈ interior s

Tactic:
refine mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩

Premises used: Iff.mpr, Metric.mem_ball_self, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, mem_interior
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s

Tactic:
hs (fun i => ?_) hz
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
intro : ∀ (i : ι), w i ≤ z i
⊢ w ∈ s

Tactic:
refine hs (fun i => ?_) hz
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
i : ι
⊢ Membership.mem (γ := Set (ι → ℝ)) (pi (α := fun (b : ι) ↦ ℝ) univ fun (b : ι) ↦ Ioo (y b - δ) (y b + δ)) w

Tactic:
simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw

Premises used: Real.ball_eq_Ioo, ball_pi
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
i : ι
hw : Membership.mem (γ := Set (ι → ℝ)) (pi (α := fun (b : ι) ↦ ℝ) univ fun (b : ι) ↦ Ioo (y b - δ) (y b + δ)) w
⊢ w i ≤ z i

Tactic:
((hw _ <| mem_univ _).2.trans <| hyz _).le

Premises used: LT.lt.le, And.right, Set.mem_univ, LT.lt.trans
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
i : ι
hw : Membership.mem (γ := Set (ι → ℝ)) (pi (α := fun (b : ι) ↦ ℝ) univ fun (b : ι) ↦ Ioo (y b - δ) (y b + δ)) w
⊢ w i ≤ z i

Tactic:
exact ((hw _ <| mem_univ _).2.trans <| hyz _).le

Premises used: LT.lt.le, And.right, Set.mem_univ, LT.lt.trans
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
x y : ι → ℝ
⊢ dist (x ⊓ y) (x ⊔ y) = dist x y

Tactic:
congr_arg NNReal.toReal (Finset.sup_congr rfl fun i _ ↦ ?_)

Premises used: congr_arg, Finset.sup_congr, NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
x y : ι → ℝ
refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)
⊢ dist (x ⊓ y) (x ⊔ y) = dist x y

Tactic:
refine congr_arg NNReal.toReal (Finset.sup_congr rfl fun i _ ↦ ?_)

Premises used: congr_arg, Finset.sup_congr, NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
x y : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)

Tactic:
simp only [Real.nndist_eq', max_sub_min_eq_abs, Pi.inf_apply,
    Pi.sup_apply, Real.nnabs_of_nonneg, abs_nonneg, Real.toNNReal_abs]

Premises used: Real.nnabs_of_nonneg, max_sub_min_eq_abs, Pi.sup_apply, Real.toNNReal_abs, Pi.inf_apply, abs_nonneg, Real.nndist_eq'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
⊢ MonotoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Ici y)

Tactic:
fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Premises used: Iff.mpr, MonotoneOn, Finset.sup_mono_fun, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
refine :
  ∀ (y₁ : ι → ℝ) (hy₁ : y₁ ∈ Ici y) (y₂ : ι → ℝ) (hy₂ : y₂ ∈ Ici y) (hy : y₁ ≤ y₂) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)
⊢ MonotoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Ici y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Premises used: Iff.mpr, Finset.sup_mono_fun, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw : (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)

Tactic:
rw [Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
    Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))]

Premises used: sub_nonneg_of_le, Real.nnabs_of_nonneg, Real.nndist_eq
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
grw grw₁ : (y₂ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
⊢ (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal

Tactic:
grw [hy i]
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
x : ι → ℝ
⊢ MonotoneOn (dist x) (Ici x)

Tactic:
simpa only [dist_comm] using dist_mono_left_pi (y := x)

Premises used: dist_comm, dist_mono_left_pi
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
⊢ AntitoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Iic y)

Tactic:
fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Premises used: Iff.mpr, Finset.sup_mono_fun, AntitoneOn, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
refine :
  ∀ (y₁ : ι → ℝ) (hy₁ : y₁ ∈ Iic y) (y₂ : ι → ℝ) (hy₂ : y₂ ∈ Iic y) (hy : y₁ ≤ y₂) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)
⊢ AntitoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Iic y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Premises used: Iff.mpr, Finset.sup_mono_fun, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw : (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)

Tactic:
rw [Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
    Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))]

Premises used: sub_nonneg_of_le, Real.nnabs_of_nonneg, Real.nndist_eq'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal

Tactic:
Real.toNNReal_mono (sub_le_sub_left (hy _) _)

Premises used: Real.toNNReal_mono, sub_le_sub_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal

Tactic:
exact Real.toNNReal_mono (sub_le_sub_left (hy _) _)

Premises used: Real.toNNReal_mono, sub_le_sub_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
x : ι → ℝ
⊢ AntitoneOn (dist x) (Iic x)

Tactic:
simpa only [dist_comm] using dist_anti_left_pi (y := x)

Premises used: dist_comm, dist_anti_left_pi
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
a₁ a₂ b₁ b₂ : ι → ℝ
ha : a₂ ≤ a₁
h₁ : a₁ ≤ b₁
hb : b₁ ≤ b₂
⊢ dist a₁ b₁ ≤ dist a₂ b₂

Tactic:
(dist_mono_right_pi h₁ (h₁.trans hb) hb).trans <|
    dist_anti_left_pi (ha.trans <| h₁.trans hb) (h₁.trans hb) ha

Premises used: LE.le.trans, dist_mono_right_pi, dist_anti_left_pi
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, Function.const, OfNat.ofNat, Metric.closedBall_subset_closedBall'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
refine_2 : closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
refine ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + ‖3 / 4 * δ‖ ≤ δ
⊢ δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ

Tactic:
grw [dist_self_add_left, ← const_def, pi_norm_const_le]

Premises used: Function.const_def, dist_self_add_left, pi_norm_const_le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + ‖3 / 4 * δ‖ = δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ

Tactic:
simp [abs_of_nonneg, hδ.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_2 :
  ∀ (y : ι → ℝ) (hy : y ∈ s) (hxy : dist x y < δ / 4), closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)

Premises used: Metric.mem_closure_iff, Iff.mp, zero_lt_four, div_pos
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_

Premises used: subset_closure, Set.Subset, IsUpperSet.mem_interior_of_forall_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
refine_2 : ∀ (z : ι → ℝ) (hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)) (i : ι), y i < z i
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_

Premises used: subset_closure, IsUpperSet.mem_interior_of_forall_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)
i : ι
refine_2 : ∀ (hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), y i < z i
⊢ y i < z i

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hz

Premises used: dist_eq_norm', Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
refine_2 : ∀ (hxy : ‖x - y‖ < δ / 4) (z : ι → ℝ) (hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), y i < z i
⊢ y i < z i

Tactic:
rw [dist_eq_norm] at hxy

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ ‖(x - y) i‖ ≤ δ / 4

Tactic:
replace hxy := (norm_le_pi_norm _ i).trans hxy.le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
⊢ ‖(x + const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4

Tactic:
replace hz := (norm_le_pi_norm _ i).trans hz
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : |x i - y i| ≤ δ / 4
hz : |x i + 3 / 4 * δ - z i| ≤ δ / 4
⊢ x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4

Tactic:
rw [abs_sub_le_iff] at hxy hz

Premises used: abs_sub_le_iff
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : |x i - y i| ≤ δ / 4
hz : |x i + 3 / 4 * δ - z i| ≤ δ / 4
hxy₁ : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
⊢ x i + 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i + 3 / 4 * δ) ≤ δ / 4

Tactic:
rw [abs_sub_le_iff] at hxy hz

Premises used: abs_sub_le_iff
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
hz : x i + 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i + 3 / 4 * δ) ≤ δ / 4
linarith : z i ≤ y i → 4 / 4 = 1
linarith₁ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : z i ≤ y i → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : z i ≤ y i → 4 / 4 = 1
linarith₄ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : z i ≤ y i → GT.gt (α := ℝ) 4 0
linarith₆ : z i ≤ y i → 4 / 4 = 1
linarith₇ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : z i ≤ y i → HMul.hMul (α := ℝ) 4 1 = 4
linarith₉ : z i ≤ y i → 4 / 4 = 1
linarith₁₀ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₁ : z i ≤ y i → GT.gt (α := ℝ) 4 0
linarith₁₂ : z i ≤ y i → 4 / 4 = 1
linarith₁₃ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₄ : z i ≤ y i → GT.gt (α := ℝ) 4 0
linarith₁₅ : z i ≤ y i → 4 / 4 = 1
linarith₁₆ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₇ : z i ≤ y i → GT.gt (α := ℝ) 4 0
linarith₁₈ :
  z i ≤ y i →
    0 - δ + (4 * y i - 4 * x i - 1 * δ) + (4 * x i + HMul.hMul (α := ℝ) 1 3 * (1 * δ) - 4 * z i - 1 * δ) +
        4 * (z i - y i) =
      0
linarith₁₉ : z i ≤ y i → GT.gt (α := ℝ) 4 0
⊢ y i < z i

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, And.intro, Exists.intro, Function.const, OfNat.ofNat, Metric.closedBall_subset_closedBall'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
refine_2 : closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + ‖3 / 4 * δ‖ ≤ δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ

Tactic:
grw [dist_self_sub_left, ← const_def, pi_norm_const_le]

Premises used: Function.const_def, dist_self_sub_left, pi_norm_const_le
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + ‖3 / 4 * δ‖ = δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_1 : δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ

Tactic:
simp [abs_of_nonneg, hδ.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
refine_2 :
  ∀ (y : ι → ℝ) (hy : y ∈ s) (hxy : dist x y < δ / 4), closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)

Premises used: Metric.mem_closure_iff, Iff.mp, zero_lt_four, div_pos
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_

Premises used: subset_closure, Set.Subset, IsLowerSet.mem_interior_of_forall_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
refine_2 : ∀ (z : ι → ℝ) (hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)) (i : ι), z i < y i
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s

Tactic:
refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_

Premises used: subset_closure, IsLowerSet.mem_interior_of_forall_lt
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)
i : ι
refine_2 : ∀ (hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), z i < y i
⊢ z i < y i

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hz

Premises used: dist_eq_norm', Metric.mem_closedBall