awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.AddTorsor
Goal:
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q_1 : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q_1
inst_5 : NormedAddTorsor W Q_1
Q : Type u_6
inst_6 : VAdd V Q
inst_7 : VSub V Q
inst_8 : Nonempty Q
inst_9 : PseudoMetricSpace Q
f : Q → P
hf : Injective f
vadd : ∀ (c : V) (x : Q), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y
norm : ∀ (x y : Q), dist x y = dist (f x) (f y)
x y : Q
⊢ dist x y = ‖x -ᵥ y‖

Tactic:
simp [norm, NormedAddTorsor.dist_eq_norm', vsub]

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_1 : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
inst_3 : SeminormedAddCommGroup W
inst_4 : PseudoMetricSpace Q_1
inst_5 : NormedAddTorsor W Q_1
Q : Type u_6
inst_6 : VAdd V Q
inst_7 : VSub V Q
inst_8 : PseudoMetricSpace Q
f : P → Q
hf : Surjective f
vadd : ∀ (c : V) (x : P), f (c +ᵥ x) = c +ᵥ f x
vsub : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y
norm : ∀ (x y : P), dist x y = dist (f x) (f y)
⊢ ∀ (x y : Q), dist x y = ‖x -ᵥ y‖

Tactic:
simp [hf.forall, ← norm, NormedAddTorsor.dist_eq_norm', ← vsub]

Premises used: Function.Surjective.forall, NormedAddTorsor.dist_eq_norm'
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
w : E
⊢ Membership.mem (γ := Set E) (sphere 0 r) w → Membership.mem (γ := Set E) (sphere 0 r) (-w)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
v : (↑(sphere 0 r) : Type u_1)
⊢ (↑(-v) : E) = -(↑v : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
⊢ ContinuousNeg.{u_1} (↑(sphere 0 r) : Type u_1)

Tactic:
IsInducing.subtypeVal.continuousNeg fun _ => rfl

Premises used: Topology.IsInducing.continuousNeg, rfl, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r_1 r : ℝ
w : E
⊢ Membership.mem (γ := Set E) (ball 0 r) w → Membership.mem (γ := Set E) (ball 0 r) (-w)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
v : (↑(ball 0 r) : Type u_1)
⊢ (↑(-v) : E) = -(↑v : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
⊢ ContinuousNeg.{u_1} (↑(ball 0 r) : Type u_1)

Tactic:
IsInducing.subtypeVal.continuousNeg fun _ => rfl

Premises used: Topology.IsInducing.continuousNeg, rfl, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r_1 r : ℝ
w : E
⊢ Membership.mem (γ := Set E) (closedBall 0 r) w → Membership.mem (γ := Set E) (closedBall 0 r) (-w)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
v : (↑(closedBall 0 r) : Type u_1)
⊢ (↑(-v) : E) = -(↑v : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.BallSphere
Goal:
E : Type u_1
i : SeminormedAddCommGroup E
r : ℝ
⊢ ContinuousNeg.{u_1} (↑(closedBall 0 r) : Type u_1)

Tactic:
IsInducing.subtypeVal.continuousNeg fun _ => rfl

Premises used: Topology.IsInducing.continuousNeg, rfl, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ dist a b = ‖a⁻¹ * b‖

Tactic:
SeminormedGroup.dist_eq _ _

Premises used: SeminormedGroup.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
rw : dist b a = ‖b⁻¹ * a‖
rw₁ rw₂ : ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖
⊢ dist a b = ‖b⁻¹ * a‖

Tactic:
rw [dist_comm, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, dist_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
simp : r ≤ ‖x⁻¹ * y‖
⊢ r ≤ dist x y

Tactic:
simp only [dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ x⁻¹ * y ≠ 1

Tactic:
simpa [inv_mul_eq_one] using hne

Premises used: inv_mul_eq_one
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ r ≤ ‖x⁻¹ * y‖

Tactic:
exact hr _ (by simpa [inv_mul_eq_one] using hne)
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : ‖1⁻¹ * a‖ = ‖a‖
rw₁ : ‖1 * a‖ = ‖a‖
rw₂ rw₃ : ‖a‖ = ‖a‖
⊢ dist a 1 = ‖a‖

Tactic:
rw [dist_eq_norm_inv_mul', inv_one, one_mul]

Premises used: inv_one, dist_eq_norm_inv_mul', one_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : dist a 1 = 0 ↔ ‖a‖ = 0
rw₁ rw₂ : ‖a‖ = 0 ↔ ‖a‖ = 0
⊢ Inseparable a 1 ↔ ‖a‖ = 0

Tactic:
rw [Metric.inseparable_iff, dist_one_right]

Premises used: Metric.inseparable_iff, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : dist a 1 = ‖a‖
rw₁ rw₂ : ‖a‖ = ‖a‖
⊢ dist 1 a = ‖a‖

Tactic:
rw [dist_comm, dist_one_right]

Premises used: dist_comm, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ Eq.{u_5 + 1} (α := E → ℝ) (dist 1) norm

Tactic:
funext dist_one_left

Premises used: funext, dist_one_left
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
rw : ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖
⊢ ‖a / b‖ = ‖b / a‖

Tactic:
rw [← dist_one, dist_eq_norm_inv_mul, dist_eq_norm_inv_mul']

Premises used: dist_eq_norm_inv_mul, dist_one, dist_eq_norm_inv_mul'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ = ‖a‖

Tactic:
simpa using norm_div_rev 1 a

Premises used: OfNat.ofNat, norm_div_rev
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
inl : ∀ (hn : 0 ≤ n), ‖a ^ |n|‖ = ‖a ^ n‖
inr : ∀ (hn : n ≤ 0), ‖a ^ |n|‖ = ‖a ^ n‖
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
rcases le_total 0 n with hn | hn

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : 0 ≤ n
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
simp [hn, abs_of_nonneg, abs_of_nonpos]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : n ≤ 0
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
simp [hn, abs_of_nonneg, abs_of_nonpos]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
rw : ‖HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)‖ = ‖a ^ n‖
rw₁ : ‖a ^ |n|‖ = ‖a ^ n‖
rw₂ rw₃ : ‖a ^ n‖ = ‖a ^ n‖
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖

Tactic:
rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]

Premises used: zpow_natCast, norm_zpow_abs, Int.abs_eq_natAbs
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
rw : ‖a ^ n.natAbs‖ = ‖a‖
rw₁ : ‖HPow.hPow (β := ℕ) a 1‖ = ‖a‖
rw₂ rw₃ : ‖a‖ = ‖a‖
⊢ ‖a ^ n‖ = ‖a‖

Tactic:
rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]

Premises used: norm_pow_natAbs, Int.isUnit_iff_natAbs_eq, pow_one, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedAddGroup E
n : ℤˣ
a : E
⊢ ‖n • a‖ = ‖a‖

Tactic:
norm_isUnit_zsmul a n.isUnit

Premises used: norm_isUnit_zsmul, Units.isUnit
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
rw : ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖
⊢ dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Tactic:
rw [dist_eq_norm_inv_mul, Set.apply_mulIndicator_symmDiff norm_inv']

Premises used: dist_eq_norm_inv_mul, norm_inv', Set.apply_mulIndicator_symmDiff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
simp :
  ‖if x ∈ t then (if x ∈ s then f x else 1)⁻¹ * f x else (if x ∈ s then f x else 1)⁻¹‖ =
    ‖(if x ∈ s then f x else 1) / if x ∈ t then f x else 1‖
⊢ ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖

Tactic:
simp only [Set.mulIndicator, mul_ite, mul_one]

Premises used: Set.mulIndicator, mul_ite, mul_one
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
pos : x ∈ t → x ∈ s → ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖
neg : x ∈ t → x ∉ s → ‖1⁻¹ * f x‖ = ‖1 / f x‖
pos₁ : x ∉ t → x ∈ s → ‖(f x)⁻¹‖ = ‖f x / 1‖
neg₁ : x ∉ t → x ∉ s → norm.{u_5} (E := E) 1⁻¹ = ‖1 / 1‖
⊢ ‖if x ∈ t then (if x ∈ s then f x else 1)⁻¹ * f x else (if x ∈ s then f x else 1)⁻¹‖ =
    ‖(if x ∈ s then f x else 1) / if x ∈ t then f x else 1‖

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
h : x ∈ t
h_1 : x ∈ s
⊢ ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
h : x ∈ t
h_1 : x ∉ s
⊢ ‖1⁻¹ * f x‖ = ‖1 / f x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
h : x ∉ t
h_1 : x ∈ s
⊢ ‖(f x)⁻¹‖ = ‖f x / 1‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
h : x ∉ t
h_1 : x ∉ s
⊢ norm.{u_5} (E := E) 1⁻¹ = ‖1 / 1‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a * b‖ ≤ ‖a‖ + ‖b‖

Tactic:
simpa [dist_eq_norm_inv_mul] using dist_triangle a⁻¹ 1 b

Premises used: dist_triangle, dist_eq_norm_inv_mul, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a₁ a₂ : E
r₁ r₂ : ℝ
h₁ : ‖a₁‖ ≤ r₁
h₂ : ‖a₂‖ ≤ r₂
⊢ ‖a₁ * a₂‖ ≤ r₁ + r₂

Tactic:
(norm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂

Premises used: add_le_add, LE.le.trans, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b c : E
⊢ ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Tactic:
norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl

Premises used: le_rfl, norm_mul_le_of_le', norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b c d : E
⊢ ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖

Tactic:
norm_mul_le_of_le' norm_mul₃_le' le_rfl

Premises used: le_rfl, norm_mul_le_of_le', norm_mul₃_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b c : E
⊢ ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

Tactic:
simpa using norm_mul_le' (a / b) (b / c)

Premises used: HDiv.hDiv, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a‖ ≤ ‖a / b‖ + ‖b‖

Tactic:
simpa only [div_one] using norm_div_le_norm_div_add_norm_div a b 1

Premises used: norm_div_le_norm_div_add_norm_div, OfNat.ofNat, div_one
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : 0 ≤ dist a 1
⊢ 0 ≤ ‖a‖

Tactic:
rw [← dist_one_right]

Premises used: dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1

Tactic:
dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1

Tactic:
exact dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
z : E
⊢ |‖z‖| = ‖z‖

Tactic:
abs_of_nonneg <| norm_nonneg' _

Premises used: norm_nonneg', abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
rw : dist.{u_5} (α := E) 1 1 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ norm.{u_5} (E := E) 1 = 0

Tactic:
rw [← dist_one_right, dist_self]

Premises used: dist_self, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ norm.{u_5} (E := E) 1 = 0

Tactic:
norm_one'

Premises used: norm_one'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ norm.{u_5} (E := E) 1 = 0

Tactic:
exact norm_one'

Premises used: norm_one'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : Subsingleton E
a : E
rw : norm.{u_5} (E := E) 1 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ‖a‖ = 0

Tactic:
rw [Subsingleton.elim a 1, norm_one']

Premises used: norm_one', Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a / b‖ ≤ ‖a‖ + ‖b‖

Tactic:
simpa [div_eq_mul_inv] using norm_mul_le' a b⁻¹

Premises used: div_eq_mul_inv, Inv.inv, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a₁ a₂ : E
r₁ r₂ : ℝ
H₁ : ‖a₁‖ ≤ r₁
H₂ : ‖a₂‖ ≤ r₂
⊢ ‖a₁ / a₂‖ ≤ r₁ + r₂

Tactic:
(norm_div_le a₁ a₂).trans <| add_le_add H₁ H₂

Premises used: norm_div_le, add_le_add, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ dist a b ≤ ‖a‖ + ‖b‖

Tactic:
simpa [dist_eq_norm_inv_mul] using norm_mul_le' a⁻¹ b

Premises used: dist_eq_norm_inv_mul, Inv.inv, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

Tactic:
simpa [dist_eq_norm_inv_mul] using abs_dist_sub_le a b 1

Premises used: abs_dist_sub_le, dist_eq_norm_inv_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a‖ - ‖b‖ ≤ ‖a⁻¹ * b‖

Tactic:
(le_abs_self _).trans (abs_norm_sub_norm_le_norm_inv_mul a b)

Premises used: le_abs_self, abs_norm_sub_norm_le_norm_inv_mul, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a‖ - ‖b‖ ≤ ‖a * b‖

Tactic:
simpa using norm_mul_le' (a * b) (b⁻¹)

Premises used: HMul.hMul, Inv.inv, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ dist ‖a‖ ‖b‖ ≤ ‖a⁻¹ * b‖

Tactic:
abs_norm_sub_norm_le_norm_inv_mul a b

Premises used: abs_norm_sub_norm_le_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖u‖ ≤ ‖u / v‖ + ‖v‖
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖

Tactic:
(norm_mul_le' _ _).trans_eq' ?_

Premises used: LE.le.trans_eq', norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
refine : ‖u / v * v‖ = ‖u‖
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖

Tactic:
refine (norm_mul_le' _ _).trans_eq' ?_

Premises used: LE.le.trans_eq', norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw rw₁ : ‖u‖ = ‖u‖
⊢ ‖u / v * v‖ = ‖u‖

Tactic:
rw [div_mul_cancel]

Premises used: div_mul_cancel
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖
⊢ ‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖

Tactic:
rw [add_comm, ← norm_inv' v, ← norm_inv' u]

Premises used: norm_inv', add_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖

Tactic:
(norm_mul_le' _ _).trans_eq' ?_

Premises used: LE.le.trans_eq', norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
refine : ‖u⁻¹ * v * v⁻¹‖ = ‖u⁻¹‖
⊢ ‖u⁻¹‖ ≤ ‖u⁻¹ * v‖ + ‖v⁻¹‖

Tactic:
refine (norm_mul_le' _ _).trans_eq' ?_

Premises used: LE.le.trans_eq', norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖u⁻¹ * v * v⁻¹‖ = ‖u⁻¹‖

Tactic:
group
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖v‖ ≤ ‖u‖ + ‖v / u‖
⊢ ‖v‖ ≤ ‖u‖ + ‖u / v‖

Tactic:
rw [norm_div_rev]

Premises used: norm_div_rev
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖

Tactic:
norm_le_norm_add_norm_div' v u

Premises used: norm_le_norm_add_norm_div'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖

Tactic:
exact norm_le_norm_add_norm_div' v u

Premises used: norm_le_norm_add_norm_div'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw rw₁ : ‖u‖ = ‖u‖
⊢ ‖u‖ = ‖u * v / v‖

Tactic:
rw [mul_div_cancel_right]

Premises used: mul_div_cancel_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖v‖ = ‖u⁻¹ * u * v‖
rw₁ : ‖v‖ = ‖1 * v‖
rw₂ rw₃ : ‖v‖ = ‖v‖
⊢ ‖v‖ = ‖u⁻¹ * (u * v)‖

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Premises used: inv_mul_cancel, mul_assoc, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v : E
rw : ‖u‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖
rw₁ rw₂ : ‖u * v‖ + ‖u‖ = ‖u * v‖ + ‖u‖
⊢ ‖u⁻¹‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖

Tactic:
rw [norm_inv', add_comm]

Premises used: norm_inv', add_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
apply : ‖x * y‖ ≤ ‖y‖
apply₁ : ‖y‖ ≤ ‖x * y‖
⊢ ‖x * y‖ = ‖y‖

Tactic:
apply le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖

Tactic:
simpa [h] using norm_mul_le' x y

Premises used: norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x * y‖

Tactic:
simpa [h] using norm_le_mul_norm_add' x y

Premises used: norm_le_mul_norm_add'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
apply : ‖x * y‖ ≤ ‖x‖
apply₁ : ‖x‖ ≤ ‖x * y‖
⊢ ‖x * y‖ = ‖x‖

Tactic:
apply le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖

Tactic:
simpa [h] using norm_mul_le' x y

Premises used: norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖

Tactic:
simpa [h] using norm_le_mul_norm_add x y

Premises used: norm_le_mul_norm_add
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖ = 0
rw : ‖x * y⁻¹‖ = ‖y‖
rw₁ : ‖y⁻¹‖ = ‖y‖
rw₂ rw₃ : ‖y‖ = ‖y‖
⊢ ‖x / y‖ = ‖y‖

Tactic:
rw [div_eq_mul_inv, norm_mul_eq_norm_right _ h, norm_inv']

Premises used: norm_mul_eq_norm_right, norm_inv', div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖ = 0
h₁ : ‖y⁻¹‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
rw [div_eq_mul_inv, norm_mul_eq_norm_left]

Premises used: norm_mul_eq_norm_left, div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h h₁ h₂ h₃ h₄ : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0

Tactic:
rwa [norm_inv']

Premises used: norm_inv'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
y : E
ε : ℝ
a : E
⊢ a ∈ ball y ε ↔ Membership.mem (γ := Set E) {x : E | ‖x⁻¹ * y‖ < ε} a

Tactic:
simp [dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
a : E
⊢ Membership.mem (γ := Set E) (ball 1 r) a ↔ Membership.mem (γ := Set E) {x : E | ‖x‖ < r} a

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist b a < r ↔ ‖b⁻¹ * a‖ < r
rw₁ rw₂ : ‖b⁻¹ * a‖ < r ↔ ‖b⁻¹ * a‖ < r
⊢ b ∈ ball a r ↔ ‖b⁻¹ * a‖ < r

Tactic:
rw [mem_ball, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Metric.mem_ball
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist a b < r ↔ ‖a⁻¹ * b‖ < r
rw₁ rw₂ : ‖a⁻¹ * b‖ < r ↔ ‖a⁻¹ * b‖ < r
⊢ b ∈ ball a r ↔ ‖a⁻¹ * b‖ < r

Tactic:
rw [mem_ball', dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Metric.mem_ball'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
rw : dist a 1 < r ↔ ‖a‖ < r
rw₁ rw₂ : ‖a‖ < r ↔ ‖a‖ < r
⊢ Membership.mem (γ := Set E) (ball 1 r) a ↔ ‖a‖ < r

Tactic:
rw [mem_ball, dist_one_right]

Premises used: Metric.mem_ball, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist b a ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
rw₁ rw₂ : ‖b⁻¹ * a‖ ≤ r ↔ ‖b⁻¹ * a‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r

Tactic:
rw [mem_closedBall, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
rw : dist a 1 ≤ r ↔ ‖a‖ ≤ r
rw₁ rw₂ : ‖a‖ ≤ r ↔ ‖a‖ ≤ r
⊢ Membership.mem (γ := Set E) (closedBall 1 r) a ↔ ‖a‖ ≤ r

Tactic:
rw [mem_closedBall, dist_one_right]

Premises used: Metric.mem_closedBall, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
rw : dist a b ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
rw₁ rw₂ : ‖a⁻¹ * b‖ ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r

Tactic:
rw [mem_closedBall', dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Metric.mem_closedBall'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ closedBall a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ ≤ ‖a‖ + r

Tactic:
simp [mem_closedBall_iff_norm_inv_mul_le.1 h]

Premises used: mem_closedBall_iff_norm_inv_mul_le, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

Tactic:
norm_le_of_mem_closedBall'

Premises used: Set.Mem, Metric.closedBall, norm_le_of_mem_closedBall'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ ball a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ < ‖a‖ + r

Tactic:
simp [mem_ball_iff_norm_inv_mul_lt.1 h]

Premises used: mem_ball_iff_norm_inv_mul_lt, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Tactic:
simpa using norm_mul_le' (u / v) (v / w)

Premises used: HDiv.hDiv, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

Tactic:
simpa [-tsub_le_iff_right, tsub_le_iff_left, two_mul, add_assoc]
    using norm_mul₃_le' (a := (u / v)) (b := v) (c := v)

Premises used: add_assoc, two_mul, tsub_le_iff_left, tsub_le_iff_right, norm_mul₃_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity