awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y z : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖

Tactic:
solid (abs_sup_sub_sup_le_abs x y z)

Premises used: HasSolidNorm.solid, abs_sup_sub_sup_le_abs
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y z : α
⊢ ‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖

Tactic:
solid (abs_inf_sub_inf_le_abs x y z)

Premises used: HasSolidNorm.solid, abs_inf_sub_inf_le_abs
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
z x y : α
rw : ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
⊢ dist (x ⊔ z) (y ⊔ z) ≤ (↑1 : ℝ) * dist x y

Tactic:
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]

Premises used: dist_eq_norm, NNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖

Tactic:
norm_sup_sub_sup_le_norm x y z

Premises used: norm_sup_sub_sup_le_norm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖

Tactic:
exact norm_sup_sub_sup_le_norm x y z

Premises used: norm_sup_sub_sup_le_norm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ LipschitzWith.{u_1, u_1} (α := α) 1 posPart

Tactic:
lipschitzWith_sup_right 0

Premises used: lipschitzWith_sup_right, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ LipschitzWith.{u_1, u_1} (α := α) 1 negPart

Tactic:
simpa [Function.comp] using lipschitzWith_posPart.comp LipschitzWith.id.neg

Premises used: Function.comp, LipschitzWith.comp, lipschitzWith_posPart
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ Continuous.{u_1, u_1} (X := α) posPart

Tactic:
lipschitzWith_posPart.continuous

Premises used: LipschitzWith.continuous, lipschitzWith_posPart
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ Continuous.{u_1, u_1} (X := α) negPart

Tactic:
lipschitzWith_negPart.continuous

Premises used: LipschitzWith.continuous, lipschitzWith_negPart
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | 0 ≤ x} x ↔ Membership.mem (γ := Set α) (negPart ⁻¹' {0}) x
⊢ Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x : α
⊢ Membership.mem (γ := Set α) {x : α | 0 ≤ x} x ↔ Membership.mem (γ := Set α) (negPart ⁻¹' {0}) x

Tactic:
simp [negPart_eq_zero]

Premises used: negPart_eq_zero
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})

Tactic:
have : {x : α | 0 ≤ x} = negPart ⁻¹' {0} := by ext; simp [negPart_eq_zero]
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
this : Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
rw : IsClosed (X := α) (negPart ⁻¹' {0})
⊢ IsClosed.{u_1} (X := α) {x : α | 0 ≤ x}

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
this : Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
⊢ IsClosed (X := α) (negPart ⁻¹' {0})

Tactic:
isClosed_singleton.preimage continuous_negPart

Premises used: continuous_negPart, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
this : Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
⊢ IsClosed (X := α) (negPart ⁻¹' {0})

Tactic:
exact isClosed_singleton.preimage continuous_negPart

Premises used: continuous_negPart, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
h₁ :
  ∀ (p : G × G),
    Membership.mem (γ := Set (G × G)) {p : G × G | p.1 ≤ p.2} p ↔
      Membership.mem (γ := Set (G × G)) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x}) p
⊢ Eq.{u_2 + 1} (α := Set (G × G)) {p : G × G | p.1 ≤ p.2}
    (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})

Tactic:
ext1 p
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
p : G × G
⊢ Membership.mem (γ := Set (G × G)) {p : G × G | p.1 ≤ p.2} p ↔
    Membership.mem (γ := Set (G × G)) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x}) p

Tactic:
simp only [sub_nonneg, Set.preimage_setOf_eq]

Premises used: Set.preimage_setOf_eq, sub_nonneg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
⊢ Eq.{u_2 + 1} (α := Set (G × G)) {p : G × G | p.1 ≤ p.2}
    (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})

Tactic:
have : { p : G × G | p.fst ≤ p.snd } = (fun p : G × G ↦ p.snd - p.fst) ⁻¹' { x : G | 0 ≤ x } := by
    ext1 p; simp only [sub_nonneg, Set.preimage_setOf_eq]
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
this :
  Eq.{u_2 + 1} (α := Set (G × G)) {p : G × G | p.1 ≤ p.2}
    (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})
rw : IsClosed.{u_2} (X := G × G) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})
⊢ IsClosed.{u_2} (X := G × G) {p : G × G | p.1 ≤ p.2}

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
this :
  Eq.{u_2 + 1} (α := Set (G × G)) {p : G × G | p.1 ≤ p.2}
    (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})
⊢ IsClosed.{u_2} (X := G × G) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})

Tactic:
IsClosed.preimage (continuous_snd.sub continuous_fst) h

Premises used: continuous_snd, continuous_fst, IsClosed.preimage, Continuous.sub
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : TopologicalSpace G
inst_4 : ContinuousSub G
h : IsClosed.{u_2} (X := G) {x : G | 0 ≤ x}
this :
  Eq.{u_2 + 1} (α := Set (G × G)) {p : G × G | p.1 ≤ p.2}
    (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})
⊢ IsClosed.{u_2} (X := G × G) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})

Tactic:
exact IsClosed.preimage (continuous_snd.sub continuous_fst) h

Premises used: continuous_snd, continuous_fst, IsClosed.preimage, Continuous.sub
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
E : Type u_2
inst_4 : NormedAddCommGroup E
inst_5 : Lattice E
inst_6 : HasSolidNorm E
inst_7 : IsOrderedAddMonoid E
⊢ OrderClosedTopology E

Tactic:
⟨isClosed_le_of_isClosed_nonneg isClosed_nonneg⟩

Premises used: isClosed_nonneg, OrderClosedTopology.mk, isClosed_le_of_isClosed_nonneg
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
rw : IsUpperSet (ball 1 ε * s)
⊢ IsUpperSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Premises used: ball_mul_one
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)

Tactic:
hs.mul_left

Premises used: IsUpperSet.mul_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)

Tactic:
exact hs.mul_left

Premises used: IsUpperSet.mul_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
rw : IsLowerSet (ball 1 ε * s)
⊢ IsLowerSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Premises used: ball_mul_one
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)

Tactic:
hs.mul_left

Premises used: IsLowerSet.mul_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)

Tactic:
exact hs.mul_left

Premises used: IsLowerSet.mul_left
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
rw : IsUpperSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
⊢ IsUpperSet (cthickening ε s)

Tactic:
rw [cthickening_eq_iInter_thickening'']

Premises used: Metric.cthickening_eq_iInter_thickening''
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)

Tactic:
isUpperSet_iInter₂ fun δ _ => hs.thickening' _

Premises used: IsUpperSet.thickening', isUpperSet_iInter₂
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)

Tactic:
exact isUpperSet_iInter₂ fun δ _ => hs.thickening' _

Premises used: IsUpperSet.thickening', isUpperSet_iInter₂
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
rw : IsLowerSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
⊢ IsLowerSet (cthickening ε s)

Tactic:
rw [cthickening_eq_iInter_thickening'']

Premises used: Metric.cthickening_eq_iInter_thickening''
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)

Tactic:
isLowerSet_iInter₂ fun δ _ => hs.thickening' _

Premises used: isLowerSet_iInter₂, IsLowerSet.thickening'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)

Tactic:
exact isLowerSet_iInter₂ fun δ _ => hs.thickening' _

Premises used: isLowerSet_iInter₂, IsLowerSet.thickening'
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
⊢ (↑(upperClosure (interior s)) : Set α) ⊆ interior (↑(upperClosure s) : Set α)

Tactic:
upperClosure_min (interior_mono subset_upperClosure) (upperClosure s).upper.interior

Premises used: subset_upperClosure, interior_mono, IsUpperSet.interior, upperClosure, upperClosure_min, UpperSet.upper
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
⊢ (↑(lowerClosure (interior s)) : Set α) ⊆ interior (↑(lowerClosure s) : Set α)

Tactic:
lowerClosure_min (interior_mono subset_lowerClosure) (lowerClosure s).lower.interior

Premises used: subset_lowerClosure, interior_mono, lowerClosure_min, LowerSet.lower, lowerClosure, IsLowerSet.interior
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
intro : ∀ (val : Fintype ι), y ∈ interior s
⊢ y ∈ interior s

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
intro : ∀ (ε : ℝ) (hε : 0 < ε) (hxy : ∀ (i : ι), x i + ε < y i), y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h

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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
intro : ∀ (z : ι → ℝ) (hz : z ∈ s) (hxz : dist x z < ε), y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε

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

Tactic:
rw [dist_pi_lt_iff hε] at hxz

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

Tactic:
fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans ?_)

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

Tactic:
refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans ?_)

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

Tactic:
rw [← Real.norm_eq_abs, ← dist_eq_norm']

Premises used: dist_eq_norm', Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), z i < y i

Tactic:
have hyz : ∀ i, z i < y i := by
    refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz : ∀ (i : ι), z i < y i
intro : ∀ (δ : ℝ) (hδ : 0 < δ) (hyz : ∀ (i : ι), z i + δ < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
intro : ∀ (i : ι), z i ≤ w 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y 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 : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz_1 : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
i : ι
hw : Membership.mem (γ := Set (ι → ℝ)) (pi (α := fun (b : ι) ↦ ℝ) univ fun (b : ι) ↦ Ioo (y b - δ) (y b + δ)) w
⊢ z i ≤ w i

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

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

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

Premises used: Iff.mpr, LT.lt.le, And.left, Set.mem_univ, LT.lt.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
intro : ∀ (val : Fintype ι), y ∈ interior s
⊢ y ∈ interior s

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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 ι
intro : ∀ (ε : ℝ) (hε : 0 < ε) (hxy : ∀ (i : ι), y i + ε < x i), y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h

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
intro : ∀ (z : ι → ℝ) (hz : z ∈ s) (hxz : dist x z < ε), y ∈ interior s
⊢ y ∈ interior s

Tactic:
obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε

Premises used: Metric.mem_closure_iff, Iff.mp
-- 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 : dist x z < ε
⊢ ∀ (b : ι), dist (x b) (z b) < ε

Tactic:
rw [dist_pi_lt_iff hε] at hxz

Premises used: dist_pi_lt_iff