awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
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:
simp [algebraMap_left_apply]

Premises used: WithAbs.algebraMap_left_apply
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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 T R
inst_5 : Algebra.IsSeparable T R
⊢ Algebra.IsSeparable.{u_3, u_1} T (WithAbs v)

Tactic:
AlgEquiv.Algebra.isSeparable (algEquiv T v).symm

Premises used: AlgEquiv.symm, WithAbs.algEquiv, AlgEquiv.Algebra.isSeparable
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
v : AbsoluteValue R S
x y : R
⊢ toAbs v (x / y) = toAbs v x / toAbs v y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
v : AbsoluteValue R S
x y : WithAbs v
⊢ (x / y).ofAbs = x.ofAbs / y.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
v : AbsoluteValue R S
x : R
⊢ toAbs v x⁻¹ = (toAbs v x)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : Field R
v : AbsoluteValue R S
x : WithAbs v
⊢ x⁻¹.ofAbs = x.ofAbs⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
inst : Field R
v : AbsoluteValue R ℝ
a : R
ha : LT.lt (α := ℝ) ((v : (a : R) → ℝ) a : ℝ) (1 : ℝ)
⊢ Filter.Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖1⁻¹ + toAbs v a ^ e - 1‖) Filter.atTop (𝓝 0)

Tactic:
simpa using ha
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
R : Type u_1
inst : Field R
v : AbsoluteValue R ℝ
a : R
ha : LT.lt (α := ℝ) ((v : (a : R) → ℝ) a : ℝ) (1 : ℝ)
⊢ Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ ((equiv v).symm : (a : R) → WithAbs v) (1 / (1 + a ^ n)))
    Filter.atTop (𝓝 1)

Tactic:
simpa using inv_one (G := WithAbs v) ▸ (tendsto_inv_iff₀ one_ne_zero).2
    (tendsto_iff_norm_sub_tendsto_zero.2 <| by simpa using ha)
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
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
⊢ UniformContinuous (β := WithAbs w) fun (x : WithAbs w) ↦ r • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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) ↦
    HMul.hMul (α := WithAbs w) ((algebraMap R (WithAbs w) : (a : R) → WithAbs w) r : WithAbs w) x

Tactic:
(Ring.uniformContinuousConstSMul _).uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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) ↦
    HMul.hMul (α := WithAbs w) ((algebraMap R (WithAbs w) : (a : R) → WithAbs w) r : WithAbs w) x

Tactic:
exact (Ring.uniformContinuousConstSMul _).uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
⊢ Isometry.{u_3, u_4} (α := WithAbs v) (β := L) (⇑f : (a : WithAbs v) → L)

Tactic:
AddMonoidHomClass.isometry_of_norm _ h

Premises used: AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
h₁ : ∀ (x x_1 : WithAbs v), dist x x_1 = dist x x_1
⊢ Eq.{u_3 + 1} (α := PseudoMetricSpace (WithAbs v))
    (PseudoMetricSpace.induced.{u_3, u_4} (β := L) (⇑f : (a : WithAbs v) → L) inferInstance)
    MetricSpace.toPseudoMetricSpace

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
x x_1 : WithAbs v
⊢ dist x x_1 = dist x x_1

Tactic:
AddMonoidHomClass.isometry_of_norm _ h |>.dist_eq _ _

Premises used: AddMonoidHomClass.isometry_of_norm, Isometry.dist_eq
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
x x_1 : WithAbs v
⊢ dist x x_1 = dist x x_1

Tactic:
exact AddMonoidHomClass.isometry_of_norm _ h |>.dist_eq _ _

Premises used: AddMonoidHomClass.isometry_of_norm, Isometry.dist_eq
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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} (α := UniformSpace (WithAbs v))
    (UniformSpace.comap.{u_3, u_4} (β := L) (⇑f : (a : WithAbs v) → L) inferInstance) PseudoMetricSpace.toUniformSpace

Tactic:
IsUniformInducing.comap_uniformSpace
    (AddMonoidHomClass.isometry_of_norm _ h).isUniformInducing

Premises used: AddMonoidHomClass.isometry_of_norm, IsUniformInducing.comap_uniformSpace, Isometry.isUniformInducing
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
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
⊢ IsUniformInducing.{u_3, u_4} (α := WithAbs v) (β := L) (⇑f : (a : WithAbs v) → L)

Tactic:
(AddMonoidHomClass.isometry_of_norm _ h).isUniformInducing

Premises used: AddMonoidHomClass.isometry_of_norm, Isometry.isUniformInducing
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_2
inst_1 : NormedField L
inst_2 : CompleteSpace L
f : RingHom.{u_1, u_2} (WithAbs v) L
h : ∀ (x : WithAbs v), norm.{u_2} (E := L) ((f : (a : WithAbs v) → L) x : L) = (v : (a : K) → ℝ) x.ofAbs
x : K
⊢ Eq.{u_2 + 1} (α := L)
    ((Isometry.extensionHom ⋯ : (a : UniformSpace.Completion (WithAbs v)) → L)
        (↑(toAbs v x) : UniformSpace.Completion (WithAbs v)) :
      L)
    ((f : (a : WithAbs v) → L) (((equiv v).symm : (a : K) → WithAbs v) x : WithAbs v) : L)

Tactic:
AddMonoidHomClass.isometry_of_norm _ h |>.extensionHom_coe _

Premises used: Isometry.extensionHom_coe, AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_2
inst_1 : NormedField L
inst_2 : CompleteSpace L
f : RingHom.{u_1, u_2} (WithAbs v) L
h : ∀ (x : WithAbs v), norm.{u_2} (E := L) ((f : (a : WithAbs v) → L) x : L) = (v : (a : K) → ℝ) x.ofAbs
x y : v.Completion
⊢ let f : RingHom.{u_1, u_2} (UniformSpace.Completion (WithAbs v)) L := Isometry.extensionHom ⋯;
  dist.{u_2} (α := L) ((f : (a : UniformSpace.Completion (WithAbs v)) → L) x : L)
      ((f : (a : UniformSpace.Completion (WithAbs v)) → L) y : L) =
    dist x y

Tactic:
AddMonoidHomClass.isometry_of_norm _ h |>.completion_extension.dist_eq _ _

Premises used: AddMonoidHomClass.isometry_of_norm, Isometry.completion_extension, UniformSpace.Completion.extension, Isometry.dist_eq, AbstractCompletion.extend, ite
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_2
inst_1 : NormedField L
inst_2 : CompleteSpace L
f : RingHom.{u_1, u_2} (WithAbs v) L
h : ∀ (x : WithAbs v), norm.{u_2} (E := L) ((f : (a : WithAbs v) → L) x : L) = (v : (a : K) → ℝ) x.ofAbs
⊢ Isometry.{u_1, u_2} (α := UniformSpace.Completion (WithAbs v)) (β := L)
    (⇑(Isometry.extensionHom ⋯) : (a : UniformSpace.Completion (WithAbs v)) → L)

Tactic:
AddMonoidHomClass.isometry_of_norm _ h |>.completion_extension

Premises used: AddMonoidHomClass.isometry_of_norm, Set.Mem, setOf, Isometry.completion_extension, UniformSpace.Completion.extension, AbstractCompletion.extend, ite
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_2
inst_1 : NormedField L
inst_2 : CompleteSpace L
f : RingHom.{u_1, u_2} (WithAbs v) L
h : ∀ (x : WithAbs v), norm.{u_2} (E := L) ((f : (a : WithAbs v) → L) x : L) = (v : (a : K) → ℝ) x.ofAbs
⊢ IsClosedEmbedding.{u_1, u_2} (X := UniformSpace.Completion (WithAbs v)) (Y := L)
    (⇑(Isometry.extensionHom ⋯) : (a : UniformSpace.Completion (WithAbs v)) → L)

Tactic:
(AddMonoidHomClass.isometry_of_norm _ h).completion_extension.isClosedEmbedding

Premises used: AddMonoidHomClass.isometry_of_norm, Isometry.completion_extension, UniformSpace.Completion.extension, Isometry.isClosedEmbedding, AbstractCompletion.extend, ite
-- Module: Mathlib.Analysis.Normed.Field.WithAbs
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
L : Type u_2
inst_1 : NormedField L
inst_2 : CompleteSpace L
f : RingHom.{u_1, u_2} (WithAbs v) L
inst_3 : LocallyCompactSpace L
h : Isometry.{u_1, u_2} (α := WithAbs v) (β := L) (⇑f : (a : WithAbs v) → L)
⊢ LocallyCompactSpace.{u_1} v.Completion

Tactic:
h.completion_extension.isClosedEmbedding.locallyCompactSpace

Premises used: Isometry.completion_extension, Isometry.isClosedEmbedding, Topology.IsClosedEmbedding.locallyCompactSpace
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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)
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)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
⊢ 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:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x t : ℝ
ht : t ≠ 0
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)})
⊢ 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:
simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]

Premises used: QuotientAddGroup.norm_eq_infDist, smul_zero, infDist_smul₀, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x t : ℝ
ht : t ≠ 0
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)}
⊢ 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:
congr 1 with m
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x t : ℝ
ht : t ≠ 0
m : ℝ
inr :
  Membership.mem (γ := Set ℝ)
      {m : ℝ |
        Membership.mem (γ := AddSubgroup ℝ)
          { carrier := HSMul.hSMul (β := Set ℝ) t (range fun (i : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑i : ℝ) p), add_mem' := ⋯,
            zero_mem' := ⋯, neg_mem' := ⋯ }
          (m - t • x)}
      m ↔
    m ∈
      HSMul.hSMul (β := Set ℝ) t
        {m : ℝ |
          Membership.mem (γ := AddSubgroup ℝ)
            { carrier := range fun (x : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑x : ℝ) p, add_mem' := ⋯, zero_mem' := ⋯,
              neg_mem' := ⋯ : AddSubgroup ℝ }
            (m - x)}
⊢ 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:
simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]

Premises used: zsmul_eq_mul, QuotientAddGroup.eq_iff_sub_mem, mul_left_comm, AddSubgroup.zmultiples, Set.range_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ Membership.mem (γ := Set ℝ)
      {m : ℝ |
        Membership.mem (γ := AddSubgroup ℝ)
          { carrier := HSMul.hSMul (β := Set ℝ) t (range fun (i : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑i : ℝ) p), add_mem' := ⋯,
            zero_mem' := ⋯, neg_mem' := ⋯ }
          (m - t • x)}
      m ↔
    m ∈
      HSMul.hSMul (β := Set ℝ) t
        {m : ℝ |
          Membership.mem (γ := AddSubgroup ℝ)
            { carrier := range fun (x : ℤ) ↦ HSMul.hSMul (α := ℝ) (↑x : ℝ) p, add_mem' := ⋯, zero_mem' := ⋯,
              neg_mem' := ⋯ : AddSubgroup ℝ }
            (m - x)}

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀ ht, mul_sub, ht]

Premises used: mul_sub, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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)
rw :
  norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-p)) =
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑(-1 * 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)

Tactic:
rw [← this, neg_one_mul]

Premises used: neg_one_mul
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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))) (↑(-1 * x) : ℝ ⧸ zmultiples (-p))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
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)
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples (-p))) (↑x : ℝ ⧸ zmultiples (-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
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x : ℝ
⊢ 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:
simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

Premises used: abs_neg, AddCircle.norm_coe_mul, abs_one, one_mul
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
this :
  Eq (α := Set ℝ)
    {y : ℝ |
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
        (↑x : ℝ ⧸ zmultiples 0)}
    {x}
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) = |x|

Tactic:
simp [norm_eq_infDist, this]

Premises used: QuotientAddGroup.norm_eq_infDist
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
suffices :
  Eq (α := Set ℝ)
    {y : ℝ |
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
        (↑x : ℝ ⧸ zmultiples 0)}
    {x}
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) = |x|

Tactic:
suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
    simp [norm_eq_infDist, this]
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
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
⊢ Eq (α := Set ℝ)
    {y : ℝ |
      Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑y : ℝ ⧸ zmultiples 0)
        (↑x : ℝ ⧸ zmultiples 0)}
    {x}

Tactic:
ext y
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x 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:
simp [eq_iff_sub_mem, sub_eq_zero]

Premises used: QuotientAddGroup.eq_iff_sub_mem, sub_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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|
inr :
  ∀ (hp : p ≠ 0),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples p) =
      |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ 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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x : ℝ
this :
  ∀ (x : ℝ),
    norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) (↑x : ℝ ⧸ zmultiples 1) =
      |x - (↑(round x) : ℝ)|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) (↑x : ℝ ⧸ zmultiples 0) =
    |x - HMul.hMul (α := ℝ) (↑(round (0⁻¹ * x)) : ℝ) 0|

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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⁻¹ * 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⁻¹
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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)
⊢ |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

Premises used: Iff.mpr, abs_inv, eq_inv_mul_iff_mul_eq₀, abs_eq_zero, not_congr
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
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|
inr₃ : |p * (p⁻¹ * x - (↑(round (p⁻¹ * x)) : ℝ))| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₄ : |p * (p⁻¹ * x) - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₅ : |x - p * (↑(round (p⁻¹ * x)) : ℝ)| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
inr₆ inr₇ : |x - (↑(round (p⁻¹ * x)) : ℝ) * p| = |x - (↑(round (p⁻¹ * x)) : ℝ) * p|
⊢ norm (E := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) (↑x : ℝ ⧸ zmultiples 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]

Premises used: mul_inv_cancel_left₀, mul_sub, abs_mul, mul_comm, inv_mul_cancel₀