awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
rw :
  p *
      |p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) -
          (↑(round (p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p))) : ℝ)| =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
rw₁ :
  p * |HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) - (↑(round (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))) : ℝ)| =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
rw₂ rw₃ :
  p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ) =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p))
      (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) : ℝ ⧸ zmultiples p) =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)

Tactic:
rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]

Premises used: abs_sub_round_div_natCast_eq, AddCircle.norm_eq', Fact.out
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
change : ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑(addOrderOf u) : ℝ)

Tactic:
change ∃ k : ℕ, ‖u‖ = p * (k / n)
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
obtain :
  ∀ (m : ℕ) (hm : (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) = u),
    ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu

Premises used: AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) = u
⊢ ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
⟨min (m % n) (n - m % n), ?_⟩

Premises used: HSub.hSub, HMod.hMod, Exists.intro, Min.min
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) = u
refine : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
⊢ ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
refine ⟨min (m % n) (n - m % n), ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) = u
rw :
  norm (E := AddCircle p) (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
rw₁ rw₂ :
  p * HDiv.hDiv (α := ℝ) (↑(min (m % addOrderOf u) (addOrderOf u - m % addOrderOf u)) : ℝ) (↑(addOrderOf u) : ℝ) =
    p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
⊢ ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)

Tactic:
rw [← hm, norm_div_natCast]

Premises used: AddCircle.norm_div_natCast
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
obtain : ∀ (n : ℕ) (hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)), p ≤ addOrderOf u • ‖u‖
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu

Premises used: AddCircle.exists_norm_eq_of_isOfFinAddOrder
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
norm_cast : ¬addOrderOf u = 0
⊢ Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
⊢ ¬addOrderOf u = 0

Tactic:
(addOrderOf_pos_iff.mpr hu).ne'

Premises used: Iff.mpr, LT.lt.ne', addOrderOf_pos_iff
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
⊢ ¬addOrderOf u = 0

Tactic:
exact (addOrderOf_pos_iff.mpr hu).ne'

Premises used: Iff.mpr, LT.lt.ne', addOrderOf_pos_iff
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
⊢ Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0

Tactic:
replace hu : (addOrderOf u : ℝ) ≠ 0 := by
    norm_cast
    exact (addOrderOf_pos_iff.mpr hu).ne'
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
hu : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
rw : p * 1
| p

Tactic:
rw [← mul_one p]

Premises used: mul_one
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
hu : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
conv_lhs : p * 1 ≤ addOrderOf u • ‖u‖
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
conv_lhs => rw [← mul_one p]

Premises used: mul_one
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
hu : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
rw : n ≠ 0
⊢ p * 1 ≤ addOrderOf u • ‖u‖

Tactic:
rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu,
    mul_le_mul_iff_right₀ hp.out, Nat.one_le_cast, Nat.one_le_iff_ne_zero]

Premises used: mul_assoc, Nat.one_le_cast, mul_div_cancel₀, mul_comm, nsmul_eq_mul, Nat.one_le_iff_ne_zero, Fact.out, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
hu : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
contrapose : ∀ (hu' : n = 0), u = 0
⊢ n ≠ 0

Tactic:
contrapose hu'
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
hu : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
hu' : n = 0
⊢ u = 0

Tactic:
simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn

Premises used: norm_eq_zero, zero_div, MulZeroClass.mul_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
    |x - (↑(round x) : ℝ)|

Tactic:
simp [AddCircle.norm_eq]

Premises used: AddCircle.norm_eq
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
c : V
x y : P
⊢ dist (c +ᵥ x) (c +ᵥ y) = dist x y

Tactic:
simp [NormedAddTorsor.dist_eq_norm']

Premises used: NormedAddTorsor.dist_eq_norm'
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
x y : P × Q
⊢ dist x y = ‖x -ᵥ y‖

Tactic:
simp only [Prod.dist_eq, NormedAddTorsor.dist_eq_norm', Prod.norm_def, Prod.fst_vsub,
      Prod.snd_vsub]

Premises used: Prod.fst_vsub, Prod.dist_eq, Prod.norm_def, Prod.snd_vsub, NormedAddTorsor.dist_eq_norm'
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y : P
⊢ dist x y = ‖x -ᵥ y‖

Tactic:
NormedAddTorsor.dist_eq_norm' x y

Premises used: NormedAddTorsor.dist_eq_norm'
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y : P
⊢ nndist x y = ‖x -ᵥ y‖₊

Tactic:
NNReal.eq <| dist_eq_norm_vsub V x y

Premises used: NNReal.eq, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y : P
⊢ dist x y = ‖y -ᵥ x‖

Tactic:
(dist_comm _ _).trans (dist_eq_norm_vsub _ _ _)

Premises used: dist_comm, dist_eq_norm_vsub, Eq.trans
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y : P
⊢ nndist x y = ‖y -ᵥ x‖₊

Tactic:
NNReal.eq <| dist_eq_norm_vsub' V x y

Premises used: dist_eq_norm_vsub', NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x y : P
⊢ dist (v +ᵥ x) (v +ᵥ y) = dist x y

Tactic:
dist_vadd _ _ _

Premises used: dist_vadd
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x y : P
⊢ nndist (v +ᵥ x) (v +ᵥ y) = nndist x y

Tactic:
NNReal.eq <| dist_vadd_cancel_left _ _ _

Premises used: NNReal.eq, dist_vadd_cancel_left
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v₁ v₂ : V
x : P
rw : ‖(v₁ +ᵥ x) -ᵥ (v₂ +ᵥ x)‖ = dist v₁ v₂
rw₁ : ‖(v₁ +ᵥ x) -ᵥ (v₂ +ᵥ x)‖ = ‖v₁ - v₂‖
rw₂ rw₃ : ‖v₁ - v₂‖ = ‖v₁ - v₂‖
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]

Premises used: dist_eq_norm, vadd_vsub_vadd_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v₁ v₂ : V
x : P
⊢ nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂

Tactic:
NNReal.eq <| dist_vadd_cancel_right _ _ _

Premises used: dist_vadd_cancel_right, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x : P
⊢ dist (v +ᵥ x) x = ‖v‖

Tactic:
simp [dist_eq_norm_vsub V _ x]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x : P
⊢ nndist (v +ᵥ x) x = ‖v‖₊

Tactic:
NNReal.eq <| dist_vadd_left _ _

Premises used: NNReal.eq, dist_vadd_left
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x : P
rw : dist (v +ᵥ x) x = ‖v‖
rw₁ rw₂ : ‖v‖ = ‖v‖
⊢ dist x (v +ᵥ x) = ‖v‖

Tactic:
rw [dist_comm, dist_vadd_left]

Premises used: dist_comm, dist_vadd_left
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v : V
x : P
⊢ nndist x (v +ᵥ x) = ‖v‖₊

Tactic:
NNReal.eq <| dist_vadd_right _ _

Premises used: NNReal.eq, dist_vadd_right
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y z : P
rw : ‖x -ᵥ y - (x -ᵥ z)‖ = dist y z
rw₁ : ‖z -ᵥ y‖ = dist y z
rw₂ : ‖z -ᵥ y‖ = dist z y
rw₃ rw₄ : ‖z -ᵥ y‖ = ‖z -ᵥ y‖
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]

Premises used: dist_eq_norm, dist_comm, vsub_sub_vsub_cancel_left, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y z : P
⊢ nndist (x -ᵥ y) (x -ᵥ z) = nndist y z

Tactic:
NNReal.eq <| dist_vsub_cancel_left _ _ _

Premises used: dist_vsub_cancel_left, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y z : P
⊢ dist (x -ᵥ z) (y -ᵥ z) = dist x y

Tactic:
(IsometryEquiv.vaddConst z).symm.dist_eq x y

Premises used: IsometryEquiv.symm, IsometryEquiv.vaddConst, IsometryEquiv.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
x y z : P
⊢ nndist (x -ᵥ z) (y -ᵥ z) = nndist x y

Tactic:
NNReal.eq <| dist_vsub_cancel_right _ _ _

Premises used: NNReal.eq, dist_vsub_cancel_right
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v v' : V
p p' : P
⊢ dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'

Tactic:
simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')

Premises used: dist_triangle, HVAdd.hVAdd
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

Tactic:
dist_vadd_vadd_le _ _ _ _

Premises used: dist_vadd_vadd_le
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
rw : ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]

Premises used: dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖

Tactic:
exact norm_sub_le _ _

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Tactic:
simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

Premises used: NNReal.coe_add, dist_nndist, dist_vsub_vsub_le, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v v' : V
p p' : P
simp : (↑(nndist (v +ᵥ p) (v' +ᵥ p')) : ENNReal) ≤ (↑(nndist v v') : ENNReal) + (↑(nndist p p') : ENNReal)
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

Tactic:
simp only [edist_nndist]

Premises used: edist_nndist
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v v' : V
p p' : P
norm_cast : nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
⊢ (↑(nndist (v +ᵥ p) (v' +ᵥ p')) : ENNReal) ≤ (↑(nndist v v') : ENNReal) + (↑(nndist p p') : ENNReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

Tactic:
apply dist_vadd_vadd_le

Premises used: dist_vadd_vadd_le
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
simp : (↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) : ENNReal) ≤ (↑(nndist p₁ p₃) : ENNReal) + (↑(nndist p₂ p₄) : ENNReal)
⊢ edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄

Tactic:
simp only [edist_nndist]

Premises used: edist_nndist
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
norm_cast : nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
⊢ (↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) : ENNReal) ≤ (↑(nndist p₁ p₃) : ENNReal) + (↑(nndist p₂ p₄) : ENNReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

Tactic:
apply dist_vsub_vsub_le

Premises used: dist_vsub_vsub_le
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : SeminormedAddCommGroup V
inst_7 : AddTorsor V P
x : P
⊢ ‖x -ᵥ x‖ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : SeminormedAddCommGroup V
inst_7 : AddTorsor V P
x y : P
⊢ ‖x -ᵥ y‖ = ‖y -ᵥ x‖

Tactic:
simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]

Premises used: norm_neg, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : SeminormedAddCommGroup V
inst_7 : AddTorsor V P
x y z : P
rw : ‖x -ᵥ y + (y -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
p₂ : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖

Tactic:
rw [← vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : NormedAddCommGroup V
inst_7 : AddTorsor V P
x : P
⊢ ‖x -ᵥ x‖ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : NormedAddCommGroup V
inst_7 : AddTorsor V P
x y : P
⊢ ‖x -ᵥ y‖ = ‖y -ᵥ x‖

Tactic:
simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]

Premises used: norm_neg, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : NormedAddCommGroup V
inst_7 : AddTorsor V P
x y z : P
rw : ‖x -ᵥ y + (y -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
p₂ : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖

Tactic:
rw [← vsub_add_vsub_cancel]

Premises used: vsub_add_vsub_cancel
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V_1 : Type u_2
P_1 : Type u_3
W : Type u_4
Q : Type u_5
inst : SeminormedAddCommGroup V_1
inst_1 : PseudoMetricSpace P_1
inst_2 : NormedAddTorsor V_1 P_1
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q
inst_5 : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst_6 : NormedAddCommGroup V
inst_7 : AddTorsor V P
x y : P
h : ‖x -ᵥ y‖ = 0
⊢ x = y

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : PseudoEMetricSpace α
f : α → V
g : α → P
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) (f +ᵥ g)

Tactic:
fun x y =>
  calc
    edist (f x +ᵥ g x) (f y +ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
      edist_vadd_vadd_le _ _ _ _
    _ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf x y) (hg x y)
    _ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm

Premises used: add_mul, ENNReal.ofNNReal, Trans.trans, LipschitzWith, add_le_add, WithTop.map₂, WithTop.some, edist_vadd_vadd_le, EDist.edist, Eq.symm, Option.map₂
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : PseudoEMetricSpace α
f g : α → P
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) (f -ᵥ g)

Tactic:
fun x y =>
  calc
    edist (f x -ᵥ g x) (f y -ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
      edist_vsub_vsub_le _ _ _ _
    _ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf x y) (hg x y)
    _ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm

Premises used: add_mul, ENNReal.ofNNReal, Trans.trans, LipschitzWith, add_le_add, WithTop.map₂, WithTop.some, EDist.edist, Eq.symm, edist_vsub_vsub_le, Option.map₂
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
⊢ UniformContinuous (β := P) fun (x : V × P) ↦ x.1 +ᵥ x.2

Tactic:
(LipschitzWith.prod_fst.vadd LipschitzWith.prod_snd).uniformContinuous

Premises used: LipschitzWith.prod_snd, Set.Mem, setOf, LipschitzWith.prod_fst, LipschitzWith.vadd, LipschitzWith.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
V : Type u_2
P : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
⊢ UniformContinuous.{u_3, u_2} (β := V) fun (x : P × P) ↦ x.1 -ᵥ x.2

Tactic:
(LipschitzWith.prod_fst.vsub LipschitzWith.prod_snd).uniformContinuous

Premises used: LipschitzWith.prod_snd, Set.Mem, setOf, LipschitzWith.prod_fst, LipschitzWith.uniformContinuous, LipschitzWith.vsub