awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
refine_2 : ∀ (hxy : ‖x - y‖ < δ / 4) (z : ι → ℝ) (hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4) (i : ι), z i < y i
⊢ z i < y 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 : 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 : ι
⊢ ‖(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 : 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
⊢ ‖(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 : 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
⊢ 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 : 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
⊢ 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 : 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
linarith₅ : y i ≤ z i → GT.gt (α := ℝ) 4 0
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
linarith₁₁ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₁₂ : y i ≤ z i → 4 / 4 = 1
linarith₁₃ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₄ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₁₅ : y i ≤ z i → 4 / 4 = 1
linarith₁₆ : y i ≤ z i → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₇ : y i ≤ z i → GT.gt (α := ℝ) 4 0
linarith₁₈ :
  y i ≤ z i →
    0 - δ + (4 * x i - 4 * y i - 1 * δ) + (4 * z i - (4 * x i - HMul.hMul (α := ℝ) 1 3 * (1 * δ)) - 1 * δ) +
        4 * (y i - z i) =
      0
linarith₁₉ : y i ≤ z i → GT.gt (α := ℝ) 4 0
⊢ z i < y i

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
intro : ∀ (val : Fintype ι), IsClosed (↑(upperClosure s) : Set (ι → ℝ))
⊢ IsClosed (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
⊢ IsClosed (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
intro :
  ∀ (f : ℕ → ι → ℝ) (x : ι → ℝ) (hf : ∀ (n : ℕ), f n ∈ (↑(upperClosure s) : Set (ι → ℝ)))
    (hx : Filter.Tendsto f Filter.atTop (nhds x)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
⊢ IsClosed (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ (↑(upperClosure s) : Set (ι → ℝ))
hx : Filter.Tendsto f Filter.atTop (nhds x)
intro :
  ∀ (g : (n : ℕ) → ι → ℝ) (hg : ∀ (n : ℕ), g n ∈ s) (hgf : ∀ (n : ℕ), g n ≤ f n), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
choose g hg hgf using hf
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
intro : ∀ (a : ι → ℝ) (ha : a ∈ upperBounds (range f)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
obtain ⟨a, ha⟩ := hx.bddAbove_range

Premises used: Filter.Tendsto.bddAbove_range
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
intro :
  ∀ (b : ι → ℝ) (hb : b ∈ closure (s ∩ Iic a)) (φ : ℕ → ℕ) (hφ : StrictMono φ)
    (hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)), x ∈ (↑(upperClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddAbove_Iic) fun n ↦
    ⟨hg n, (hgf _).trans <| ha <| mem_range_self _⟩

Premises used: Set.mem_range_self, BddBelow.isBounded_inter, And.intro, LE.le.trans, tendsto_subseq_of_bounded, bddAbove_Iic
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Iic a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
⟨b, closure_minimal inter_subset_left hs hb,
    le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_atTop) fun _ ↦ hgf _⟩

Premises used: Set.Mem, closure_minimal, setOf, StrictMono.tendsto_atTop, Set.inter_subset_left, And.intro, Exists.intro, le_of_tendsto_of_tendsto', Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddBelow s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hgf : ∀ (n : ℕ), g n ≤ f n
a : ι → ℝ
ha : a ∈ upperBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Iic a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
exact ⟨b, closure_minimal inter_subset_left hs hb,
    le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_atTop) fun _ ↦ hgf _⟩
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
intro : ∀ (val : Fintype ι), IsClosed (↑(lowerClosure s) : Set (ι → ℝ))
⊢ IsClosed (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
⊢ IsClosed (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
intro :
  ∀ (f : ℕ → ι → ℝ) (x : ι → ℝ) (hf : ∀ (n : ℕ), f n ∈ (↑(lowerClosure s) : Set (ι → ℝ)))
    (hx : Filter.Tendsto f Filter.atTop (nhds x)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
⊢ IsClosed (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hf : ∀ (n : ℕ), f n ∈ (↑(lowerClosure s) : Set (ι → ℝ))
hx : Filter.Tendsto f Filter.atTop (nhds x)
intro :
  ∀ (g : (n : ℕ) → ι → ℝ) (hg : ∀ (n : ℕ), g n ∈ s) (hfg : ∀ (n : ℕ), f n ≤ g n), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
choose g hg hfg using hf
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
⊢ BoundedGENhdsClass ℝ

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
⊢ BoundedGENhdsClass ℝ

Tactic:
haveI : BoundedGENhdsClass ℝ := by infer_instance
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
intro : ∀ (a : ι → ℝ) (ha : a ∈ lowerBounds (range f)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
obtain ⟨a, ha⟩ := hx.bddBelow_range

Premises used: Filter.Tendsto.bddBelow_range
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
a : ι → ℝ
ha : a ∈ lowerBounds (range f)
intro :
  ∀ (b : ι → ℝ) (hb : b ∈ closure (s ∩ Ici a)) (φ : ℕ → ℕ) (hφ : StrictMono φ)
    (hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)), x ∈ (↑(lowerClosure s) : Set (ι → ℝ))
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddBelow_Ici) fun n ↦
    ⟨hg n, (ha <| mem_range_self _).trans <| hfg _⟩

Premises used: Set.mem_range_self, bddBelow_Ici, BddAbove.isBounded_inter, And.intro, LE.le.trans, tendsto_subseq_of_bounded
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
a : ι → ℝ
ha : a ∈ lowerBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Ici a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
⟨b, closure_minimal inter_subset_left hs hb,
    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_atTop) hbf fun _ ↦ hfg _⟩

Premises used: Set.Mem, closure_minimal, setOf, StrictMono.tendsto_atTop, Set.inter_subset_left, And.intro, Exists.intro, le_of_tendsto_of_tendsto', Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : (n : ℕ) → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
a : ι → ℝ
ha : a ∈ lowerBounds (range f)
b : ι → ℝ
hb : b ∈ closure (s ∩ Ici a)
φ : ℕ → ℕ
hφ : StrictMono φ
hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)
⊢ x ∈ (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
exact ⟨b, closure_minimal inter_subset_left hs hb,
    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_atTop) hbf fun _ ↦ hfg _⟩
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClopen s
hs' : BddBelow s
⊢ IsClopen (↑(upperClosure s) : Set (ι → ℝ))

Tactic:
⟨hs.1.upperClosure_pi hs', hs.2.upperClosure⟩

Premises used: IsOpen.upperClosure, And.right, And.left, And.intro, IsClopen, IsClosed.upperClosure_pi
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : IsClopen s
hs' : BddAbove s
⊢ IsClopen (↑(lowerClosure s) : Set (ι → ℝ))

Tactic:
⟨hs.1.lowerClosure_pi hs', hs.2.lowerClosure⟩

Premises used: IsOpen.lowerClosure, IsClosed.lowerClosure_pi, And.right, And.left, And.intro, IsClopen
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : BddBelow s
⊢ closure (↑(upperClosure s) : Set (ι → ℝ)) = (↑(upperClosure (closure s)) : Set (ι → ℝ))

Tactic:
(closure_minimal (upperClosure_anti subset_closure) <|
      isClosed_closure.upperClosure_pi hs.closure).antisymm <|
    upperClosure_min (closure_mono subset_upperClosure) (upperClosure s).upper.closure

Premises used: BddBelow.closure, subset_upperClosure, subset_closure, closure_minimal, upperClosure, setOf, closure_mono, upperClosure_min, HasSubset.Subset.antisymm, UpperSet.upper, isClosed_closure, IsClosed.upperClosure_pi, IsUpperSet.closure, upperClosure_anti
-- Module: Mathlib.Analysis.Normed.Order.UpperLower
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
hs : BddAbove s
⊢ closure (↑(lowerClosure s) : Set (ι → ℝ)) = (↑(lowerClosure (closure s)) : Set (ι → ℝ))

Tactic:
(closure_minimal (lowerClosure_mono subset_closure) <|
        isClosed_closure.lowerClosure_pi hs.closure).antisymm <|
    lowerClosure_min (closure_mono subset_lowerClosure) (lowerClosure s).lower.closure

Premises used: subset_lowerClosure, IsClosed.lowerClosure_pi, subset_closure, closure_minimal, IsLowerSet.closure, closure_mono, BddAbove.closure, HasSubset.Subset.antisymm, lowerClosure_min, isClosed_closure, LowerSet.lower, lowerClosure, lowerClosure_mono
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x x_1 : PUnit.{u_5 + 1}
⊢ ‖x * x_1‖ ≤ ‖x‖ * ‖x_1‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
inst_1 : One G
inst_2 : NormOneClass G
⊢ nnnorm.{u_1} (E := G) 1 = 1

Tactic:
NNReal.eq norm_one

Premises used: NormOneClass.norm_one, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
inst_1 : One G
inst_2 : NormOneClass G
⊢ enorm.{u_1} (E := G) 1 = 1

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
inst_1 : One G
inst_2 : NormOneClass G
⊢ norm.{u_1} (E := G) 0 ≠ norm.{u_1} (E := G) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : One α
inst_2 : NormOneClass α
⊢ Norm.norm (E := ULift.{u_5, u_2} α) 1 = 1

Tactic:
simp [ULift.norm_def]

Premises used: ULift.norm_def
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : One α
inst_2 : NormOneClass α
inst_3 : SeminormedAddCommGroup β
inst_4 : One β
inst_5 : NormOneClass β
⊢ norm (E := α × β) 1 = 1

Tactic:
simp [Prod.norm_def]

Premises used: Prod.norm_def
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α_1 : Type u_2
β : Type u_3
ι_1 : Type u_4
ι : Type u_5
α : ι → Type u_6
inst : Nonempty ι
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
inst_3 : (i : ι) → One (α i)
inst_4 : ∀ (i : ι), NormOneClass.{u_6} (α i)
⊢ norm (E := (i : ι) → α i) 1 = 1

Tactic:
simpa [Pi.norm_def] using Finset.sup_const Finset.univ_nonempty 1

Premises used: Finset.univ_nonempty, Finset.sup_const, Pi.norm_def, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : One α
inst_2 : NormOneClass α
⊢ NormOneClass.{u_2} αᵐᵒᵖ

Tactic:
⟨@norm_one α _ _ _⟩

Premises used: NormOneClass.mk, NormOneClass.norm_one
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖ ≤ ‖a‖ * ‖b‖

Tactic:
NonUnitalSeminormedRing.norm_mul_le a b

Premises used: NonUnitalSeminormedRing.norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊

Tactic:
norm_mul_le a b

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a₁ a₂ : α
r₁ r₂ : ℝ
h₁ : ‖a₁‖ ≤ r₁
h₂ : ‖a₂‖ ≤ r₂
⊢ ‖a₁ * a₂‖ ≤ r₁ * r₂

Tactic:
(norm_mul_le ..).trans <| mul_le_mul h₁ h₂ (norm_nonneg _) ((norm_nonneg _).trans h₁)

Premises used: mul_le_mul, LE.le.trans, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a₁ a₂ : α
r₁ r₂ : ℝ≥0
h₁ : ‖a₁‖₊ ≤ r₁
h₂ : ‖a₂‖₊ ≤ r₂
⊢ ‖a₁ * a₂‖₊ ≤ r₁ * r₂

Tactic:
(nnnorm_mul_le ..).trans <| mul_le_mul' h₁ h₂

Premises used: nnnorm_mul_le, LE.le.trans, mul_le_mul'
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a b c : α
⊢ ‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖

Tactic:
norm_mul_le_of_le (norm_mul_le ..) le_rfl

Premises used: le_rfl, norm_mul_le, norm_mul_le_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
a b c : α
⊢ ‖a * b * c‖₊ ≤ ‖a‖₊ * ‖b‖₊ * ‖c‖₊

Tactic:
nnnorm_mul_le_of_le (norm_mul_le ..) le_rfl

Premises used: le_rfl, norm_mul_le, nnnorm_mul_le_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
β : Type u_5
inst : NormedRing β
inst_1 : Nontrivial β
⊢ norm.{u_5} (E := β) 1 ≤ norm.{u_5} (E := β) 1 * norm.{u_5} (E := β) 1

Tactic:
simpa only [mul_one] using norm_mul_le (1 : β) 1

Premises used: mul_one, norm_mul_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
β : Type u_5
inst : NormedRing β
inst_1 : Nontrivial β
⊢ 1 ≤ nnnorm.{u_5} (E := β) 1

Tactic:
one_le_norm_one β

Premises used: one_le_norm_one
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
x : α
⊢ ∀ (y : α), norm (E := α) ((AddMonoidHom.mulLeft x : (a : α) → α) y : α) ≤ ‖x‖ * ‖y‖

Tactic:
norm_mul_le x

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
x y : α
rw : norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖y‖ * ‖x‖
⊢ norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖x‖ * ‖y‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
x y : α
⊢ norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖y‖ * ‖x‖

Tactic:
norm_mul_le y x

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NonUnitalSeminormedRing α
x y : α
⊢ norm (E := α) ((AddMonoidHom.mulRight x : (a : α) → α) y : α) ≤ ‖y‖ * ‖x‖

Tactic:
exact norm_mul_le y x

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖x.2‖ * ‖y.2‖) = max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
ha : 0 ≤ ‖x.1‖
hd : 0 ≤ ‖y.2‖
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖

Tactic:
apply max_mul_mul_le_max_mul_max

Premises used: max_mul_mul_le_max_mul_max
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖x.1‖

Tactic:
simp [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖y.2‖

Tactic:
simp [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst_1 : NonUnitalSeminormedRing β
x y : α × β
⊢ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖ = max ‖x.1‖ ‖x.2‖ * max ‖y.1‖ ‖y.2‖

Tactic:
simp [max_comm]

Premises used: max_comm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
⊢ norm.{u_2} (E := α) (↑0 : α) ≤ (↑0 : ℝ) * norm.{u_2} (E := α) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
n : ℕ
rw : ‖HAdd.hAdd (α := α) (↑n : α) 1‖ ≤ (↑n : ℝ) * norm.{u_2} (E := α) 1 + norm.{u_2} (E := α) 1
⊢ norm.{u_2} (E := α) (↑(n + 1) : α) ≤ (↑(n + 1) : ℝ) * norm.{u_2} (E := α) 1

Tactic:
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, one_mul
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
n : ℕ
⊢ ‖HAdd.hAdd (α := α) (↑n : α) 1‖ ≤ (↑n : ℝ) * norm.{u_2} (E := α) 1 + norm.{u_2} (E := α) 1

Tactic:
norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

Premises used: le_rfl, norm_add_le_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
n : ℕ
⊢ ‖HAdd.hAdd (α := α) (↑n : α) 1‖ ≤ (↑n : ℝ) * norm.{u_2} (E := α) 1 + norm.{u_2} (E := α) 1

Tactic:
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

Premises used: le_rfl, norm_add_le_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a : α
h : [a] ≠ []
⊢ ‖[a].prod‖ ≤ (map norm [a]).prod

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
rw : ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod
⊢ ‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod

Tactic:
le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))

Premises used: norm_mul_le, mul_le_mul_of_nonneg_left, norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
refine : ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod

Tactic:
refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))

Premises used: norm_mul_le, mul_le_mul_of_nonneg_left, le_trans
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod

Tactic:
List.norm_prod_le' (List.cons_ne_nil b l)

Premises used: List.cons_ne_nil