awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
h : -x + z = -x + (y + (-y + z))
h₁ : -x + z = -x + (y + -y + z)
h₂ : -x + z = -x + (0 + z)
⊢ -x + z = -x + y + (-y + z)
have h₃ : -x + z = -x + z
Tactic: rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖
have a₁ : |a| ≤ |b|
Tactic: apply solid
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|
have a₁ : a ⊔ -a ≤ |b|
Tactic: rw [abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|
have a₁ : - -a ⊔ -a ≤ |b|
Tactic: nth_rw 1 [← neg_neg a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|
have a₁ : -(-a ⊓ a) ≤ |b|
Tactic: rw [← neg_inf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|
have a₁ : -(-a ⊓ a) ≤ b ⊔ -b
Tactic: rw [abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b
have a₁ : -(-a ⊓ a) ≤ - -b ⊔ -b
Tactic: nth_rw 1 [← neg_neg b]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
have a₁ : -(-a ⊓ a) ≤ -(-b ⊓ b)
Tactic: rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
a₁ : -(-a ⊓ a) ≤ -(-b ⊓ b)
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
have a₂ : -b ⊓ b ≤ -a ⊓ a
Tactic: rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
a₁ : -(-a ⊓ a) ≤ -(-b ⊓ b)
a₂ : -b ⊓ b ≤ -a ⊓ a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
have a₃ : b ⊓ -b ≤ -a ⊓ a
Tactic: rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
have rw : ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
Tactic: rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
have refine : |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
Tactic: refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
have rw : |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
Tactic: rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
have rw : |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ d|
Tactic: rw [sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
have h₁ : |a ⊓ b - c ⊓ b| ≤ |a - c|
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
h₁ : |a ⊓ b - c ⊓ b| ≤ |a - c|
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
have h₂ : |c ⊓ b - c ⊓ d| ≤ |b - d|
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|
have h₂ : |b ⊓ c - d ⊓ c| ≤ |b - d|
Tactic: rw [inf_comm c, inf_comm c]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
have b₁ : |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
Tactic: calc
    |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_inf_sub_inf_le_abs _ _ _
      · rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
b₁ : |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
have b₂ : |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
Tactic: calc
    |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_inf_sub_inf_le_abs _ _ _
      · rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
have rw : ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
Tactic: rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
have refine : |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
Tactic: refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
have rw : |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
Tactic: rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
have rw : |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ d|
Tactic: rw [sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
have h₁ : |a ⊔ b - c ⊔ b| ≤ |a - c|
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
h₁ : |a ⊔ b - c ⊔ b| ≤ |a - c|
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
have h₂ : |c ⊔ b - c ⊔ d| ≤ |b - d|
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|
have h₂ : |b ⊔ c - d ⊔ c| ≤ |b - d|
Tactic: rw [sup_comm c, sup_comm c]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
have b₁ : |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
Tactic: calc
    |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_sup_sub_sup_le_abs _ _ _
      · rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
b₁ : |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
have b₂ : |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
Tactic: calc
    |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_sup_sub_sup_le_abs _ _ _
      · rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
Tactic: have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
Tactic: have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_sup_sub_sup_le_add_norm x y 0 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ ContinuousInf α
have refine : ∀ (q : α × α),
  Filter.Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 ⊓ e.2 - (fun (p : α × α) ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)
Tactic: refine ⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_sub_tendsto_zero.2 <| ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
q : α × α
⊢ Filter.Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 ⊓ e.2 - (fun (p : α × α) ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)
have this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
Tactic: have : ∀ p : α × α, ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖ := fun _ =>
    norm_inf_sub_inf_le_add_norm _ _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ Filter.Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 ⊓ e.2 - (fun (p : α × α) ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)
have refine : Filter.Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)
Tactic: refine squeeze_zero (fun e => norm_nonneg _) this ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ Filter.Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)
have h : 0 = ‖q.1 - q.1‖ + ‖q.2 - q.2‖
Tactic: convert!
    ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
      ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ (↑1 : ℝ) * dist x y
have rw : ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
Tactic: rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
have h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | 0 ≤ x} x ↔ Membership.mem (γ := Set α) (negPart ⁻¹' {0}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ IsClosed.{u_1} (X := α) {x : α | 0 ≤ x}
have this : Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
Tactic: have : {x : α | 0 ≤ x} = negPart ⁻¹' {0} := by ext; simp [negPart_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
this : Eq (α := Set α) {x : α | 0 ≤ x} (negPart ⁻¹' {0})
⊢ IsClosed.{u_1} (X := α) {x : α | 0 ≤ x}
have rw : IsClosed (X := α) (negPart ⁻¹' {0})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
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})
have 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
Tactic: ext1 p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (hypothesis)
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}
⊢ IsClosed.{u_2} (X := G × G) {p : G × G | p.1 ≤ p.2}
have 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})
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Lattice (goal)
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) {p : G × G | p.1 ≤ p.2}
have rw : IsClosed.{u_2} (X := G × G) (Set.preimage (β := G) (fun (p : G × G) ↦ p.2 - p.1) {x : G | 0 ≤ x})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)
have rw : IsUpperSet (ball 1 ε * s)
Tactic: rw [← ball_mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (thickening ε s)
have rw : IsLowerSet (ball 1 ε * s)
Tactic: rw [← ball_mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (cthickening ε s)
have rw : IsUpperSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
Tactic: rw [cthickening_eq_iInter_thickening'']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
α : Type u_1
inst : NormedCommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (cthickening ε s)
have rw : IsLowerSet.{u_1} (α := α) (⋂ (ε_1 : ℝ), ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
Tactic: rw [cthickening_eq_iInter_thickening'']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
Goal:
ι : Type u_2
inst : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
⊢ y ∈ interior s
have intro : ∀ (val : Fintype ι), y ∈ interior s
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 ι
⊢ y ∈ interior s
have intro : ∀ (ε : ℝ) (hε : 0 < ε) (hxy : ∀ (i : ι), x i + ε < y i), y ∈ interior s
Tactic: obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ 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 : 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 < ε
⊢ 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 : 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
have refine : ∀ (i : ι), |z i - x i| ≤ ε
Tactic: refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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 - x i| ≤ ε
have rw : dist (x i) (z i) ≤ ε
Tactic: rw [← Real.norm_eq_abs, ← dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (hypothesis)
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) < ε
⊢ y ∈ interior s
have hyz : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.UpperLower (goal)
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
⊢ y ∈ interior s
have intro : ∀ (δ : ℝ) (hδ : 0 < δ) (hyz : ∀ (i : ι), z i + δ < y 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 : 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
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 : 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
have intro : ∀ (i : ι), z i ≤ w 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 : 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 : ι
⊢ z i ≤ w 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 : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
⊢ y ∈ interior s
have intro : ∀ (val : Fintype ι), y ∈ interior s
Tactic: cases nonempty_fintype ι
-- 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 ι
⊢ y ∈ interior s
have intro : ∀ (ε : ℝ) (hε : 0 < ε) (hxy : ∀ (i : ι), y i + ε < x i), y ∈ interior s
Tactic: obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h