awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x y : α
⊢ Eq (α := ℝ) ((f : (a : α) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : α) → ℝ) (y⁻¹ * x) : ℝ)

Tactic:
simp [← map_inv_eq_map f (x⁻¹ * y)]

Premises used: HMul.hMul, GroupSeminormClass.map_inv_eq_map, Inv.inv
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x y z : α
⊢ (f : (a : α) → ℝ) (x⁻¹ * y * (y⁻¹ * z)) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : α) → ℝ) (y⁻¹ * z) : ℝ)

Tactic:
map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z)

Premises used: HMul.hMul, Inv.inv, MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x y z : α
h : x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
⊢ (f : (a : α) → ℝ) (x⁻¹ * z) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : α) → ℝ) (y⁻¹ * z) : ℝ)

Tactic:
convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2

Premises used: HMul.hMul, Inv.inv, MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x y z : α
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)

Tactic:
group
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x : α
⊢ ‖x‖ = (f : (a : α) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : CommGroup α
inst_2 : GroupSeminormClass F α ℝ
f : F
x : α
⊢ ‖x‖ = (f : (a : α) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupNormClass F α ℝ
f : F
x : α
⊢ ‖x‖ = (f : (a : α) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : CommGroup α
inst_2 : GroupNormClass F α ℝ
f : F
x : α
⊢ ‖x‖ = (f : (a : α) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Order.Hom.Ultra
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 : α
simp :
  LE.le (α := ℝ) ((f : (a : α) → ℝ) (-x + z) : ℝ) (max ((f : (a : α) → ℝ) (-x + y)) ((f : (a : α) → ℝ) (-y + z)) : ℝ)
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simp +instances only [hd, dist_eq_norm_neg_add,
      AddGroupSeminormClass.toSeminormedAddGroup_norm_eq]

Premises used: AddGroupSeminormClass.toSeminormedAddGroup_norm_eq
-- Module: Mathlib.Analysis.Normed.Order.Hom.Ultra
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 : α
⊢ LE.le (α := ℝ) ((f : (a : α) → ℝ) (-x + y + (-y + z)) : ℝ)
    (max ((f : (a : α) → ℝ) (-x + y)) ((f : (a : α) → ℝ) (-y + z)) : ℝ)

Tactic:
hna (-x + y) (-y + z)

Premises used: HAdd.hAdd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Order.Hom.Ultra
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)
⊢ LE.le (α := ℝ) ((f : (a : α) → ℝ) (-x + z) : ℝ) (max ((f : (a : α) → ℝ) (-x + y)) ((f : (a : α) → ℝ) (-y + z)) : ℝ)

Tactic:
convert! hna (-x + y) (-y + z) using 2

Premises used: HAdd.hAdd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Order.Hom.Ultra
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)
h₃ h₄ : -x + z = -x + z
⊢ -x + z = -x + y + (-y + z)

Tactic:
rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]

Premises used: add_neg_cancel, add_assoc, zero_add
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
a b : α
h : |a| ≤ |b|
⊢ ‖a‖ ≤ ‖b‖

Tactic:
HasSolidNorm.solid h

Premises used: HasSolidNorm.solid
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
r : ℝ
⊢ IsSolid.{u_1} (α := α) (Metric.ball 0 r)

Tactic:
fun _ hx _ hxy =>
  mem_ball_zero_iff.mpr ((HasSolidNorm.solid hxy).trans_lt (mem_ball_zero_iff.mp hx))

Premises used: Iff.mpr, HasSolidNorm.solid, Set.Mem, Iff.mp, LE.le.trans_lt, LatticeOrderedAddCommGroup.IsSolid, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
⊢ HasSolidNorm ℝ

Tactic:
⟨fun _ _ => id⟩

Premises used: id, HasSolidNorm.mk
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
x x_1 : ℚ
h : |x| ≤ |x_1|
⊢ ‖x‖ ≤ ‖x_1‖

Tactic:
simpa only [norm, ← Rat.cast_abs, Rat.cast_le]

Premises used: Norm.norm, Rat.cast_abs, Rat.cast_le
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
x y : ℤ
h : |x| ≤ |y|
⊢ ‖x‖ ≤ ‖y‖

Tactic:
simpa [← Int.norm_cast_real, ← Int.cast_abs] using h

Premises used: Int.cast_abs, Int.norm_cast_real
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
⊢ ‖a‖ ≤ ‖b‖

Tactic:
apply solid

Premises used: HasSolidNorm.solid
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
⊢ |a| ≤ |b|

Tactic:
rw [abs]

Premises used: abs
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
⊢ a ⊔ -a ≤ |b|

Tactic:
nth_rw 1 [← neg_neg a]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
⊢ - -a ⊔ -a ≤ |b|

Tactic:
rw [← neg_inf]

Premises used: neg_inf
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|

Tactic:
rw [abs]

Premises used: abs
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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

Tactic:
nth_rw 1 [← neg_neg b]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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₃ : b ⊓ -b ≤ -a ⊓ a
a₄ a₅ a₆ a₇ : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b

Tactic:
rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]

Premises used: inf_comm, neg_inf, neg_le_neg_iff
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ HasSolidNorm.{u_1} αᵒᵈ

Tactic:
{ solid := dual_solid (α := α) }

Premises used: HasSolidNorm.mk, dual_solid
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a : α
⊢ ‖|a|‖ = ‖a‖

Tactic:
(solid (abs_abs a).le).antisymm (solid (abs_abs a).symm.le)

Premises used: HasSolidNorm.solid, LE.le.antisymm, Eq.le, abs_abs, Eq.symm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw : ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]

Premises used: HSub.hSub, norm_abs_eq_norm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|‖

Tactic:
le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Premises used: HasSolidNorm.solid, abs, HSub.hSub, norm_add_le, le_trans
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
refine : |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Tactic:
refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Premises used: HasSolidNorm.solid, abs, HSub.hSub, norm_add_le, le_trans
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw : |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Premises used: HSub.hSub, add_nonneg, abs_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw rw₁ : |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ d|
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|

Tactic:
rw [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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 ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d|

Tactic:
abs_add_le _ _

Premises used: abs_add_le
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
h₂ : |c ⊓ b - c ⊓ d| ≤ |b - d|
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|

Tactic:
gcongr ?_ + ?_
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|

Tactic:
abs_inf_sub_inf_le_abs _ _ _

Premises used: 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 α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|

Tactic:
exact abs_inf_sub_inf_le_abs _ _ _

Premises used: 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 α
a b c d : α
h₂ : |b ⊓ c - d ⊓ c| ≤ |b - d|
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Tactic:
rw [inf_comm c, inf_comm c]

Premises used: inf_comm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|

Tactic:
abs_inf_sub_inf_le_abs _ _ _

Premises used: 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 α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|

Tactic:
exact abs_inf_sub_inf_le_abs _ _ _

Premises used: 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 α
a b c d : α
b₁ : |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
b₂ : |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
⊢ |a ⊓ 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 _ _ _

Premises used: HSub.hSub, abs_add_le, Min.min
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw : ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]

Premises used: HSub.hSub, norm_abs_eq_norm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|‖

Tactic:
le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Premises used: HasSolidNorm.solid, abs, HSub.hSub, norm_add_le, le_trans
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
refine : |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Tactic:
refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Premises used: HasSolidNorm.solid, abs, HSub.hSub, norm_add_le, le_trans
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw : |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Premises used: HSub.hSub, add_nonneg, abs_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
rw rw₁ : |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ d|
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|

Tactic:
rw [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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 ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d|

Tactic:
abs_add_le _ _

Premises used: abs_add_le
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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|
h₂ : |c ⊔ b - c ⊔ d| ≤ |b - d|
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|

Tactic:
gcongr ?_ + ?_
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

Tactic:
abs_sup_sub_sup_le_abs _ _ _

Premises used: 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 α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

Premises used: 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 α
a b c d : α
h₂ : |b ⊔ c - d ⊔ c| ≤ |b - d|
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|

Tactic:
rw [sup_comm c, sup_comm c]

Premises used: sup_comm
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|

Tactic:
abs_sup_sub_sup_le_abs _ _ _

Premises used: 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 α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

Premises used: 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 α
a b c d : α
b₁ : |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
b₂ : |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
⊢ |a ⊔ 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 _ _ _

Premises used: HSub.hSub, Max.max, abs_add_le
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
⊢ ‖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
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa only [inf_idem, sub_zero] using h

Premises used: sub_zero, inf_idem
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
⊢ ‖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
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa only [sup_idem, sub_zero] using h

Premises used: sub_zero, sup_idem
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ ContinuousInf α

Tactic:
⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_sub_tendsto_zero.2 <| ?_⟩

Premises used: Iff.mpr, ContinuousInf.mk, continuous_iff_continuousAt, tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
refine :
  ∀ (q : α × α),
    Filter.Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 ⊓ e.2 - (fun (p : α × α) ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)
⊢ ContinuousInf α

Tactic:
refine ⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_sub_tendsto_zero.2 <| ?_⟩
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
q : α × α
⊢ ∀ (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 _ _ _ _
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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)

Tactic:
squeeze_zero (fun e => norm_nonneg _) this ?_

Premises used: squeeze_zero, HSub.hSub, Prod.fst, Prod.snd, norm_nonneg, Min.min
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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‖
refine : Filter.Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)
⊢ Filter.Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 ⊓ e.2 - (fun (p : α × α) ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)

Tactic:
refine squeeze_zero (fun e => norm_nonneg _) this ?_

Premises used: squeeze_zero, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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 (x : α × α) ↦ ‖x.1 - q.1‖ + ‖x.2 - q.2‖) (nhds q) (nhds (‖q.1 - q.1‖ + ‖q.2 - q.2‖))

Tactic:
((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
      ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm

Premises used: tendsto_const_nhds, continuous_snd, continuous_fst, Filter.Tendsto.norm, Continuous.tendsto, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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‖
h : 0 = ‖q.1 - q.1‖ + ‖q.2 - q.2‖
⊢ Filter.Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)

Tactic:
convert!
    ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
      ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm

Premises used: tendsto_const_nhds, continuous_snd, continuous_fst, Filter.Tendsto.norm, Continuous.tendsto, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Order.Lattice
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‖
⊢ 0 = ‖q.1 - q.1‖ + ‖q.2 - q.2‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α_1 : Type u_1
inst : NormedAddCommGroup α_1
inst_1 : Lattice α_1
inst_2 : HasSolidNorm α_1
inst_3 : IsOrderedAddMonoid α_1
α : Type u_2
inst_4 : NormedAddCommGroup α
inst_5 : Lattice α
inst_6 : HasSolidNorm α
inst_7 : IsOrderedAddMonoid α
⊢ ContinuousSup α

Tactic:
OrderDual.continuousSup αᵒᵈ

Premises used: OrderDual, OrderDual.continuousSup
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
⊢ TopologicalLattice α

Tactic:
TopologicalLattice.mk

Premises used: TopologicalLattice.mk
-- Module: Mathlib.Analysis.Normed.Order.Lattice
Goal:
α : Type u_1
inst : NormedAddCommGroup α
inst_1 : Lattice α
inst_2 : HasSolidNorm α
inst_3 : IsOrderedAddMonoid α
a b : α
⊢ ‖|a| - |b|‖ ≤ ‖a - b‖

Tactic:
solid (abs_abs_sub_abs_le _ _)

Premises used: HasSolidNorm.solid, abs_abs_sub_abs_le