awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
this : (↑z : ℝ) * p ≤ p
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 2 / 2 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : GT.gt (α := ℝ) 2 0
⊢ False
have linarith₉ : 2 * ε - 1 * |p| + 2 * (y - (x + (↑z : ℝ) * p + ε)) + (2 * x - 1 * |p| - 2 * y) + 2 * ((↑z : ℝ) * p - p) +
    2 * (|p| - -p) =
  0
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
have rw : p⁻¹ * (p * HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
rw : p⁻¹ * (p * HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
have rw₁ : HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p : ℝ
hp : Fact (0 < p)
m 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 : ℝ)
have this : p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑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 : ℝ)
have 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 : ℝ)
Tactic: rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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 : ℝ)
⊢ 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 : ℝ)
have rw₁ : p * |HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) - (↑(round (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))) : ℝ)| =
  p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
Tactic: rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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 : ℝ)
⊢ 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 : ℝ)
have rw₂ : p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ) =
  p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
Tactic: rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)
have obtain : ∀ (m : ℕ) (hm : (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) = u),
  ∃ (k : ℕ), ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑k : ℝ) (↑n : ℝ)
Tactic: obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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 : ℝ)
have refine : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
Tactic: refine ⟨min (m % n) (n - m % n), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
have rw : norm (E := AddCircle p) (↑(HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(addOrderOf u) : ℝ) * p) : ℝ ⧸ zmultiples p) =
  p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
Tactic: rw [← hm, norm_div_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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 : ℝ)
⊢ ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑(min (m % n) (n - m % n)) : ℝ) (↑n : ℝ)
have 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 : ℝ)
Tactic: rw [← hm, norm_div_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖
have obtain : ∀ (n : ℕ) (hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)), p ≤ addOrderOf u • ‖u‖
Tactic: obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
have norm_cast : ¬addOrderOf u = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑(addOrderOf u) : ℝ)
⊢ p ≤ addOrderOf u • ‖u‖
have hu₁ : Ne (α := ℝ) (↑(addOrderOf u) : ℝ) 0
Tactic: replace hu : (addOrderOf u : ℝ) ≠ 0 := by
    norm_cast
    exact (addOrderOf_pos_iff.mpr hu).ne'
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
| p
have rw : p * 1
Tactic: rw [← mul_one p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p ≤ addOrderOf u • ‖u‖
have conv_lhs : p * 1 ≤ addOrderOf u • ‖u‖
Tactic: conv_lhs => rw [← mul_one p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p * 1 ≤ addOrderOf u • ‖u‖
have rw : n ≠ 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ n ≠ 0
have contrapose : ∀ (hu' : n = 0), u = 0
Tactic: contrapose hu'
Cleared hypotheses: hu'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
have rw : ‖(v₁ +ᵥ x) -ᵥ (v₂ +ᵥ x)‖ = dist v₁ v₂
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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₂
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
have rw₁ : ‖(v₁ +ᵥ x) -ᵥ (v₂ +ᵥ x)‖ = ‖v₁ - v₂‖
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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₂‖
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
have rw₂ : ‖v₁ - v₂‖ = ‖v₁ - v₂‖
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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 x (v +ᵥ x) = ‖v‖
have rw : dist (v +ᵥ x) x = ‖v‖
Tactic: rw [dist_comm, dist_vadd_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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‖
⊢ dist x (v +ᵥ x) = ‖v‖
have rw₁ : ‖v‖ = ‖v‖
Tactic: rw [dist_comm, dist_vadd_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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 -ᵥ y) (x -ᵥ z) = dist y z
have rw : ‖x -ᵥ y - (x -ᵥ z)‖ = dist y z
Tactic: rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z
have rw₁ : ‖z -ᵥ y‖ = dist y z
Tactic: rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z
have rw₂ : ‖z -ᵥ y‖ = dist z y
Tactic: rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z
have rw₃ : ‖z -ᵥ y‖ = ‖z -ᵥ y‖
Tactic: rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
have rw : ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
Tactic: rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
have simp : (↑(nndist (v +ᵥ p) (v' +ᵥ p')) : ENNReal) ≤ (↑(nndist v v') : ENNReal) + (↑(nndist p p') : ENNReal)
Tactic: simp only [edist_nndist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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')) : ENNReal) ≤ (↑(nndist v v') : ENNReal) + (↑(nndist p p') : ENNReal)
have norm_cast : nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
have simp : (↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) : ENNReal) ≤ (↑(nndist p₁ p₃) : ENNReal) + (↑(nndist p₂ p₄) : ENNReal)
Tactic: simp only [edist_nndist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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₄)) : ENNReal) ≤ (↑(nndist p₁ p₃) : ENNReal) + (↑(nndist p₂ p₄) : ENNReal)
have norm_cast : nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
have rw : ‖x -ᵥ y + (y -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
Tactic: rw [← vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddTorsor (goal)
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
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
have rw : ‖x -ᵥ y + (y -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
Tactic: rw [← vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ dist a b = ‖b⁻¹ * a‖
have rw : dist b a = ‖b⁻¹ * a‖
Tactic: rw [dist_comm, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
rw : dist b a = ‖b⁻¹ * a‖
⊢ dist a b = ‖b⁻¹ * a‖
have rw₁ : ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖
Tactic: rw [dist_comm, dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
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
⊢ (fun (x1 x2 : E) ↦ r ≤ dist x1 x2) x y
have simp : r ≤ ‖x⁻¹ * y‖
Tactic: simp only [dist_eq_norm_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ dist a 1 = ‖a‖
have rw : ‖1⁻¹ * a‖ = ‖a‖
Tactic: rw [dist_eq_norm_inv_mul', inv_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : ‖1⁻¹ * a‖ = ‖a‖
⊢ dist a 1 = ‖a‖
have rw₁ : ‖1 * a‖ = ‖a‖
Tactic: rw [dist_eq_norm_inv_mul', inv_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : ‖1⁻¹ * a‖ = ‖a‖
rw₁ : ‖1 * a‖ = ‖a‖
⊢ dist a 1 = ‖a‖
have rw₂ : ‖a‖ = ‖a‖
Tactic: rw [dist_eq_norm_inv_mul', inv_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ Inseparable a 1 ↔ ‖a‖ = 0
have rw : dist a 1 = 0 ↔ ‖a‖ = 0
Tactic: rw [Metric.inseparable_iff, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : dist a 1 = 0 ↔ ‖a‖ = 0
⊢ Inseparable a 1 ↔ ‖a‖ = 0
have rw₁ : ‖a‖ = 0 ↔ ‖a‖ = 0
Tactic: rw [Metric.inseparable_iff, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ dist 1 a = ‖a‖
have rw : dist a 1 = ‖a‖
Tactic: rw [dist_comm, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : dist a 1 = ‖a‖
⊢ dist 1 a = ‖a‖
have rw₁ : ‖a‖ = ‖a‖
Tactic: rw [dist_comm, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a / b‖ = ‖b / a‖
have rw : ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖
Tactic: rw [← dist_one, dist_eq_norm_inv_mul, dist_eq_norm_inv_mul']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖ = ‖a ^ n‖
have inl : ∀ (hn : 0 ≤ n), ‖a ^ |n|‖ = ‖a ^ n‖
Tactic: rcases le_total 0 n with hn | hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
inl : ∀ (hn : 0 ≤ n), ‖a ^ |n|‖ = ‖a ^ n‖
⊢ ‖a ^ |n|‖ = ‖a ^ n‖
have inr : ∀ (hn : n ≤ 0), ‖a ^ |n|‖ = ‖a ^ n‖
Tactic: rcases le_total 0 n with hn | hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖
have rw : ‖HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)‖ = ‖a ^ n‖
Tactic: rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
rw : ‖HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)‖ = ‖a ^ n‖
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖
have rw₁ : ‖a ^ |n|‖ = ‖a ^ n‖
Tactic: rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
rw : ‖HPow.hPow (β := ℤ) a (↑n.natAbs : ℤ)‖ = ‖a ^ n‖
rw₁ : ‖a ^ |n|‖ = ‖a ^ n‖
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖
have rw₂ : ‖a ^ n‖ = ‖a ^ n‖
Tactic: rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a ^ n‖ = ‖a‖
have rw : ‖a ^ n.natAbs‖ = ‖a‖
Tactic: rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
rw : ‖a ^ n.natAbs‖ = ‖a‖
⊢ ‖a ^ n‖ = ‖a‖
have rw₁ : ‖HPow.hPow (β := ℕ) a 1‖ = ‖a‖
Tactic: rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
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‖
⊢ ‖a ^ n‖ = ‖a‖
have rw₂ : ‖a‖ = ‖a‖
Tactic: rw [← norm_pow_natAbs, Int.isUnit_iff_natAbs_eq.mp hn, pow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖
have rw : ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖
Tactic: rw [dist_eq_norm_inv_mul, Set.apply_mulIndicator_symmDiff norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ‖(s.mulIndicator f x)⁻¹ * t.mulIndicator f x‖ = ‖s.mulIndicator f x / t.mulIndicator f x‖
have 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‖
Tactic: simp only [Set.mulIndicator, mul_ite, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ‖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‖
have pos : x ∈ t → x ∈ s → ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
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‖
⊢ ‖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‖
have neg : x ∈ t → x ∉ s → ‖1⁻¹ * f x‖ = ‖1 / f x‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
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‖
⊢ ‖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‖
have pos₁ : x ∉ t → x ∈ s → ‖(f x)⁻¹‖ = ‖f x / 1‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
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‖
⊢ ‖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‖
have neg₁ : x ∉ t → x ∉ s → norm.{u_5} (E := E) 1⁻¹ = ‖1 / 1‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ 0 ≤ ‖a‖
have rw : 0 ≤ dist a 1
Tactic: rw [← dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ norm.{u_5} (E := E) 1 = 0
have rw : dist.{u_5} (α := E) 1 1 = 0
Tactic: rw [← dist_one_right, dist_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedGroup E
rw : dist.{u_5} (α := E) 1 1 = 0
⊢ norm.{u_5} (E := E) 1 = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← dist_one_right, dist_self]