awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
inr : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), 1 ≤ ‖x‖
⊢ LE.le (α := ℝ) (∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k) (∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m)
have inr₁ : ∀ (i : ℕ) (hi : i ∈ Finset.range (m + 1)), i ≤ m
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1
have inl : ∀ (hm : max 1 (HPow.hPow (β := ℕ) ‖x‖ 0) = 1) (hx : HPow.hPow (β := ℕ) ‖x‖ 0 ≤ 1)
  (hi : i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1)), ‖x‖ ^ i ≤ 1
Tactic: rcases eq_or_ne m 0 with rfl | hm
Cleared hypotheses: m, hm, hx, hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
inl :
  ∀ (hm : max 1 (HPow.hPow (β := ℕ) ‖x‖ 0) = 1) (hx : HPow.hPow (β := ℕ) ‖x‖ 0 ≤ 1)
    (hi : i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1)), ‖x‖ ^ i ≤ 1
⊢ ‖x‖ ^ i ≤ 1
have inl₁ : ∀ (hm : m ≠ 0), ‖x‖ ^ i ≤ 1
Tactic: rcases eq_or_ne m 0 with rfl | hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm_1 : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1
have inl : ∀ (hx : ‖x‖ ≤ 1) (i : ℕ) (hi : i ∈ Finset.range (m + 1)) (hm : m ≠ 0), ‖x‖ ^ i ≤ 1
Tactic: rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
Cleared hypotheses: hx, i, hi, hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Ultra (goal)
Goal:
R : Type u_1
inst : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖
have inr : ∀ (hx : ‖x‖ < 1), ‖x‖ ^ m ≤ 1
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (ball 0 1) a
hy : Membership.mem (γ := Set 𝕜) (ball 0 1) b
⊢ Membership.mem (γ := Set 𝕜) (ball 0 1) (a * b)
have rw : ∀ (hx : ‖a‖ < 1) (hy : ‖b‖ < 1), ‖a * b‖ < 1
Tactic: rw [mem_ball_zero_iff] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : NonUnitalSeminormedRing 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (closedBall 0 1) a
hy : Membership.mem (γ := Set 𝕜) (closedBall 0 1) b
⊢ Membership.mem (γ := Set 𝕜) (closedBall 0 1) (a * b)
have rw : ∀ (hx : ‖a‖ ≤ 1) (hy : ‖b‖ ≤ 1), ‖a * b‖ ≤ 1
Tactic: rw [mem_closedBall_zero_iff] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜_1 : Type u_1
𝕜 : Type u_2
inst : SeminormedRing 𝕜
inst_1 : NormMulClass 𝕜
inst_2 : NormOneClass 𝕜
a b : 𝕜
hx : Membership.mem (γ := Set 𝕜) (sphere 0 1) a
hy : Membership.mem (γ := Set 𝕜) (sphere 0 1) b
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) (a * b)
have rw : ∀ (hx : ‖a‖ = 1) (hy : ‖b‖ = 1), ‖a * b‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
⊢ ‖(↑x : 𝕜)⁻¹‖ = 1
have rw : ‖(↑x : 𝕜)‖⁻¹ = 1
Tactic: rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖⁻¹ = 1
⊢ ‖(↑x : 𝕜)⁻¹‖ = 1
have rw₁ : Eq (α := ℝ) 1⁻¹ 1
Tactic: rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖⁻¹ = 1
rw₁ : Eq (α := ℝ) 1⁻¹ 1
⊢ ‖(↑x : 𝕜)⁻¹‖ = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
⊢ ‖(↑x : 𝕜) / (↑y : 𝕜)‖ = 1
have rw : ‖(↑x : 𝕜)‖ / ‖(↑y : 𝕜)‖ = 1
Tactic: rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖ / ‖(↑y : 𝕜)‖ = 1
⊢ ‖(↑x : 𝕜) / (↑y : 𝕜)‖ = 1
have rw₁ : 1 / ‖(↑y : 𝕜)‖ = 1
Tactic: rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖ / ‖(↑y : 𝕜)‖ = 1
rw₁ : 1 / ‖(↑y : 𝕜)‖ = 1
⊢ ‖(↑x : 𝕜) / (↑y : 𝕜)‖ = 1
have rw₂ : 1 / 1 = 1
Tactic: rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x y : (↑(sphere 0 1) : Type u_1)
rw : ‖(↑x : 𝕜)‖ / ‖(↑y : 𝕜)‖ = 1
rw₁ : 1 / ‖(↑y : 𝕜)‖ = 1
rw₂ : 1 / 1 = 1
⊢ ‖(↑x : 𝕜) / (↑y : 𝕜)‖ = 1
have rw₃ : Eq (α := ℝ) 1 1
Tactic: rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) ((↑x : 𝕜) ^ n)
have rw : ‖(↑x : 𝕜) ^ n‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
rw : ‖(↑x : 𝕜) ^ n‖ = 1
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) ((↑x : 𝕜) ^ n)
have rw₁ : ‖(↑x : 𝕜)‖ ^ n = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
rw : ‖(↑x : 𝕜) ^ n‖ = 1
rw₁ : ‖(↑x : 𝕜)‖ ^ n = 1
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) ((↑x : 𝕜) ^ n)
have rw₂ : HPow.hPow (α := ℝ) 1 n = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.UnitBall (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
x : (↑(sphere 0 1) : Type u_1)
n : ℤ
rw : ‖(↑x : 𝕜) ^ n‖ = 1
rw₁ : ‖(↑x : 𝕜)‖ ^ n = 1
rw₂ : HPow.hPow (α := ℝ) 1 n = 1
⊢ Membership.mem (γ := Set 𝕜) (sphere 0 1) ((↑x : 𝕜) ^ n)
have rw₃ : Eq (α := ℝ) 1 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.WithAbs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
T : Type u_3
inst_3 : Field T
v : AbsoluteValue R S
inst_4 : Algebra R T
inst_5 : Algebra.IsSeparable R T
⊢ Eq (α := R →+* T)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (WithAbs v) T) (↑(equiv v).symm : R →+* WithAbs v))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.refl T) : T →+* T) (algebraMap R T))
have a : ∀ (x : R),
  Eq.{u_3 + 1} (α := T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (WithAbs v) T)
            (↑(equiv v).symm : R →+* WithAbs v) :
          (a : R) → T)
        x :
      T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.refl T) : T →+* T) (algebraMap R T) :
          (a : R) → T)
        x :
      T)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.WithAbs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : CommRing R
T : Type u_3
inst_3 : Field T
inst_4 : Algebra R T
w : AbsoluteValue T ℝ
r : R
⊢ UniformContinuous (β := WithAbs w) fun (x : WithAbs w) ↦ r • x
have simp_rw : UniformContinuous (β := WithAbs w) fun (x : WithAbs w) ↦
  HMul.hMul (α := WithAbs w) ((algebraMap R (WithAbs w) : (a : R) → WithAbs w) r : WithAbs w) x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.WithAbs (goal)
Goal:
K : Type u_3
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst_1 : NormedField L
f : RingHom.{u_3, u_4} (WithAbs v) L
h : ∀ (x : WithAbs v), norm.{u_4} (E := L) ((f : (a : WithAbs v) → L) x : L) = (v : (a : K) → ℝ) x.ofAbs
⊢ Eq.{u_3 + 1} (α := PseudoMetricSpace (WithAbs v))
    (PseudoMetricSpace.induced.{u_3, u_4} (β := L) (⇑f : (a : WithAbs v) → L) inferInstance)
    MetricSpace.toPseudoMetricSpace
have h₁ : ∀ (x x_1 : WithAbs v), dist x x_1 = dist x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x t : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑(t * x) : ℝ ⧸ zmultiples (t * p)) =
    |t| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
have inl : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (0 * p))) (↑(0 * x) : ℝ ⧸ zmultiples (0 * p)) =
  |0| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
Tactic: obtain rfl | ht := eq_or_ne t 0
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x t : ℝ
inl :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (0 * p))) (↑(0 * x) : ℝ ⧸ zmultiples (0 * p)) =
    |0| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑(t * x) : ℝ ⧸ zmultiples (t * p)) =
    |t| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
have inr : ∀ (ht : t ≠ 0),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑(t * x) : ℝ ⧸ zmultiples (t * p)) =
    |t| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
Tactic: obtain rfl | ht := eq_or_ne t 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x t : ℝ
ht : t ≠ 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑(t * x) : ℝ ⧸ zmultiples (t * p)) =
    |t| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
have inr : infDist (α := ℝ) 0
    {m : ℝ |
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑m : ℝ ⧸ zmultiples (t * p))
        (↑(t * x) : ℝ ⧸ zmultiples (t * p))} =
  infDist 0
    (HSMul.hSMul (β := Set ℝ) t
      {m : ℝ |
        Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑m : ℝ ⧸ zmultiples p)
          (↑x : ℝ ⧸ zmultiples p)})
Tactic: simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x t : ℝ
ht : t ≠ 0
⊢ infDist (α := ℝ) 0
      {m : ℝ |
        Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑m : ℝ ⧸ zmultiples (t * p))
          (↑(t * x) : ℝ ⧸ zmultiples (t * p))} =
    infDist 0
      (HSMul.hSMul (β := Set ℝ) t
        {m : ℝ |
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑m : ℝ ⧸ zmultiples p)
            (↑x : ℝ ⧸ zmultiples p)})
have inr : ∀ (m : ℝ),
  Membership.mem (γ := Set ℝ)
      {m : ℝ |
        Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑m : ℝ ⧸ zmultiples (t * p))
          (↑(t * x) : ℝ ⧸ zmultiples (t * p))}
      m ↔
    m ∈
      HSMul.hSMul (β := Set ℝ) t
        {m : ℝ |
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑m : ℝ ⧸ zmultiples p)
            (↑x : ℝ ⧸ zmultiples p)}
Tactic: congr 1 with m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ Membership.mem (γ := Set ℝ)
      {m : ℝ |
        Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (t * p))) (↑m : ℝ ⧸ zmultiples (t * p))
          (↑(t * x) : ℝ ⧸ zmultiples (t * p))}
      m ↔
    m ∈
      HSMul.hSMul (β := Set ℝ) t
        {m : ℝ |
          Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑m : ℝ ⧸ zmultiples p)
            (↑x : ℝ ⧸ zmultiples p)}
have inr : Membership.mem (γ := Set ℝ)
    {m : ℝ |
      Membership.mem (γ := AddSubgroup ℝ)
        { carrier := HSMul.hSMul (β := Set ℝ) t (range fun (i : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑i : ℝ) p), add_mem' := sorry,
          zero_mem' := sorry, neg_mem' := sorry }
        (m - t • x)}
    m ↔
  m ∈
    HSMul.hSMul (β := Set ℝ) t
      {m : ℝ |
        Membership.mem (γ := AddSubgroup ℝ)
          { carrier := range fun (x : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑x : ℝ) p, add_mem' := sorry, zero_mem' := sorry,
            neg_mem' := sorry : AddSubgroup ℝ }
          (m - x)}
Tactic: simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-1 * p))) (↑(-1 * x) : ℝ ⧸ zmultiples (-1 * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
have rw : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) =
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑(-1 * x) : ℝ ⧸ zmultiples (-p))
Tactic: rw [← this, neg_one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
have suffices : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-1 * p))) (↑(-1 * x) : ℝ ⧸ zmultiples (-1 * p)) =
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
Tactic: suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
    rw [← this, neg_one_mul]
    simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x : ℝ
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) = |x|
have suffices : Eq (α := Set ℝ)
  {y : ℝ |
    Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
      (↑x : ℝ ⧸ zmultiples 0)}
  {x}
Tactic: suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
    simp [norm_eq_infDist, this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
x : ℝ
⊢ Eq (α := Set ℝ)
    {y : ℝ |
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
        (↑x : ℝ ⧸ zmultiples 0)}
    {x}
have h : ∀ (y : ℝ),
  Membership.mem (γ := Set ℝ)
      {y : ℝ |
        Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
          (↑x : ℝ ⧸ zmultiples 0)}
      y ↔
    Membership.mem (γ := Set ℝ) {x} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inl : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) =
  |x - HMul.hMul (α := ℝ) (↑(round (0⁻¹ * x)) : ℝ) 0|
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
inl :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) =
    |x - HMul.hMul (α := ℝ) (↑(round (0⁻¹ * x)) : ℝ) 0|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr : ∀ (hp : p ≠ 0),
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rcases eq_or_ne p 0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have hx : norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p))) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
  |p⁻¹| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
Tactic: have hx := norm_coe_mul p x p⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
      (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |p⁻¹| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have hx₁ : |p| *
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
      (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
Tactic: rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr : |p| *
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
      (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
  |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₁ : |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
  |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₁ :
  |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₂ : |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
Goal:
p x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
hp : p ≠ 0
hx :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p)
inr :
  |p| *
      norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (p⁻¹ * p)))
        (↑(p⁻¹ * x) : ℝ ⧸ zmultiples (p⁻¹ * p)) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₁ :
  |p| * norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑(p⁻¹ * x) : ℝ ⧸ zmultiples 1) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₂ : |p| * |p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
    |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
have inr₃ : |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
Tactic: rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]