awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y ∈ interior s
have intro : ∀ (z : ι → ℝ) (hz : z ∈ s) (hxz : dist x z < ε), y ∈ interior s
Tactic: obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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 : dist x z < ε
⊢ y ∈ interior s
have hxz₁ : ∀ (b : ι), dist (x b) (z b) < ε
Tactic: rw [dist_pi_lt_iff hε] at hxz
Cleared hypotheses: hxz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have refine : ∀ (i : ι), |x i - z i| ≤ ε
Tactic: refine fun i =>
      (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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) < ε
⊢ y ∈ interior s
have hyz : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y ∈ interior s
have intro : ∀ (δ : ℝ) (hδ : 0 < δ) (hyz : ∀ (i : ι), y i + δ < z i), y ∈ interior s
Tactic: obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have intro : ball y δ ⊆ s
Tactic: refine mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have intro : ∀ (i : ι), w i ≤ z i
Tactic: refine hs (fun i => ?_) hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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 : ι
⊢ w i ≤ z i
have hw₁ : 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
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
x y : ι → ℝ
⊢ dist (x ⊓ y) (x ⊔ y) = dist x y
have refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → nndist ((x ⊓ y) i) ((x ⊔ y) i) = nndist (x i) (y i)
Tactic: refine congr_arg NNReal.toReal (Finset.sup_congr rfl fun i _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
⊢ MonotoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Ici y)
have 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)
Tactic: refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)
have rw : (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
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))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
have grw : (y₂ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
Tactic: grw [hy i]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
y : ι → ℝ
⊢ AntitoneOn (β := ℝ) (fun (x : ι → ℝ) ↦ dist x y) (Iic y)
have 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)
Tactic: refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)
have rw : (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal
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))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have refine_1 : δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
Tactic: refine ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 ≤ δ
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
have refine_2 : closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
Tactic: refine ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
have refine_1 : δ / 4 + ‖3 / 4 * δ‖ ≤ δ
Tactic: grw [dist_self_add_left, ← const_def, pi_norm_const_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ
have refine_1 : δ / 4 + ‖3 / 4 * δ‖ = δ
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
have refine_1 : δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ
Tactic: simp [abs_of_nonneg, hδ.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
have refine_2 : ∀ (y : ι → ℝ) (hy : y ∈ s) (hxy : dist x y < δ / 4), 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have refine_2 : ∀ (z : ι → ℝ) (hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)) (i : ι), y i < z i
Tactic: refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 : ι
⊢ y i < z i
have refine_2 : ∀ (hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), y i < z i
Tactic: rw [mem_closedBall, dist_eq_norm'] at hz
Cleared hypotheses: hz, i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 : ι
⊢ y i < z i
have refine_2 : ∀ (hxy : ‖x - y‖ < δ / 4) (z : ι → ℝ) (hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), y i < z i
Tactic: rw [dist_eq_norm] at hxy
Cleared hypotheses: hxy, z, hz, i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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 : ι
⊢ y i < z i
have hxy₁ : ‖(x - y) i‖ ≤ δ / 4
Tactic: replace hxy := (norm_le_pi_norm _ i).trans hxy.le
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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
⊢ y i < z i
have hz₁ : ‖(x + const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
Tactic: replace hz := (norm_le_pi_norm _ i).trans hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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
⊢ y i < z i
have hxy₁ : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
Tactic: rw [abs_sub_le_iff] at hxy hz
Cleared hypotheses: hxy, hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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
⊢ y i < z i
have hz₁ : x i + 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i + 3 / 4 * δ) ≤ δ / 4
Tactic: rw [abs_sub_le_iff] at hxy hz
Cleared hypotheses: hxy, hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y i < z i
have linarith : z i ≤ y i → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y i < z i
have linarith₁ : z i ≤ y i → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y i < z i
have linarith₂ : z i ≤ y i → HMul.hMul (α := ℝ) 4 1 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y i < z i
have linarith₅ : z i ≤ y i → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y i < z i
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have refine_1 : δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
Tactic: refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 ≤ δ
⊢ ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
have refine_2 : closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
Tactic: refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
have refine_1 : δ / 4 + ‖3 / 4 * δ‖ ≤ δ
Tactic: grw [dist_self_sub_left, ← const_def, pi_norm_const_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ
have refine_1 : δ / 4 + ‖3 / 4 * δ‖ = δ
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
have refine_1 : δ / 4 + HDiv.hDiv (α := ℝ) 3 4 * δ = δ
Tactic: simp [abs_of_nonneg, hδ.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
have refine_2 : ∀ (y : ι → ℝ) (hy : y ∈ s) (hxy : dist x y < δ / 4), 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
have refine_2 : ∀ (z : ι → ℝ) (hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)) (i : ι), z i < y i
Tactic: refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 : ι
⊢ z i < y i
have refine_2 : ∀ (hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), z i < y i
Tactic: rw [mem_closedBall, dist_eq_norm'] at hz
Cleared hypotheses: hz, i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
have refine_2 : ∀ (hxy : ‖x - y‖ < δ / 4) (z : ι → ℝ) (hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), z i < y i
Tactic: rw [dist_eq_norm] at hxy
Cleared hypotheses: hxy, z, hz, i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
have hxy₁ : ‖(x - y) i‖ ≤ δ / 4
Tactic: replace hxy := (norm_le_pi_norm _ i).trans hxy.le
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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
⊢ z i < y i
have hz₁ : ‖(x - const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
Tactic: replace hz := (norm_le_pi_norm _ i).trans hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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
⊢ z i < y i
have hxy₁ : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
Tactic: rw [abs_sub_le_iff] at hxy hz
Cleared hypotheses: hxy, hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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
⊢ z i < y i
have hz₁ : x i - 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i - 3 / 4 * δ) ≤ δ / 4
Tactic: rw [abs_sub_le_iff] at hxy hz
Cleared hypotheses: hxy, hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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
⊢ z i < y i
have linarith : y i ≤ z i → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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 : y i ≤ z i → 4 / 4 = 1
⊢ z i < y i
have linarith₁ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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 : y i ≤ z i → 4 / 4 = 1
linarith₁ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
⊢ z i < y i
have linarith₂ : y i ≤ z i → HMul.hMul (α := ℝ) 4 1 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet 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 : y i ≤ z i → 4 / 4 = 1
linarith₁ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : y i ≤ z i → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : y i ≤ z i → 4 / 4 = 1
linarith₄ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
⊢ z i < y i
have linarith₅ : y i ≤ z i → GT.gt (α := ℝ) 4 0
Tactic: linarith