awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  Eq.{u_1 + 1} (α := (↑{u : AddCircle p | addOrderOf u = n} : Type u_1))
    ((fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
        (Subtype.mk (p := fun (x : AddCircle p) ↦
            Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
            (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
          { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
      m₁)
    ((fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
        (Subtype.mk (p := fun (x : AddCircle p) ↦
            Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
            (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
          { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
      m₂)
⊢ HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)

Tactic:
simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h

Premises used: Subtype.mk_eq_mk, AddCircle.natCast_div_mul_eq_nsmul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
⊢ (↑m₁ : ℕ) = (↑m₂ : ℕ)

Tactic:
nsmul_injOn_Iio_addOrderOf ?_ ?_ h

Premises used: nsmul_injOn_Iio_addOrderOf
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
refine_1 : (↑m₁ : ℕ) ∈ Iio (addOrderOf (G := AddCircle p) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p))
refine_1₁ : (↑m₂ : ℕ) ∈ Iio (addOrderOf (G := AddCircle p) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p))
⊢ (↑m₁ : ℕ) = (↑m₂ : ℕ)

Tactic:
refine nsmul_injOn_Iio_addOrderOf ?_ ?_ h

Premises used: nsmul_injOn_Iio_addOrderOf
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
refine_1 : (↑m₁ : ℕ) ∈ Iio n
⊢ (↑m₁ : ℕ) ∈ Iio (addOrderOf (G := AddCircle p) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p))

Tactic:
rw [addOrderOf_period_div hn]

Premises used: AddCircle.addOrderOf_period_div
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
refine_1 : (↑m₂ : ℕ) ∈ Iio n
⊢ (↑m₂ : ℕ) ∈ Iio (addOrderOf (G := AddCircle p) (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p))

Tactic:
rw [addOrderOf_period_div hn]

Premises used: AddCircle.addOrderOf_period_div
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
⊢ (↑m₁ : ℕ) ∈ Iio n

Tactic:
m₁.2.1

Premises used: Set.Mem, setOf, And.left, Set.Iio, Nat.lt, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
⊢ (↑m₂ : ℕ) ∈ Iio n

Tactic:
m₂.2.1

Premises used: Set.Mem, setOf, And.left, Set.Iio, Nat.lt, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)
h :
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₁ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑m₂ : ℕ)
      (↑(p / (↑n : 𝕜)) : 𝕜 ⧸ zmultiples p)
⊢ (↑m₁ : ℕ) ∈ Iio n

Tactic:
exacts [m₁.2.1, m₂.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : (↑{u : AddCircle p | addOrderOf u = n} : Type u_1)
refine_2 :
  ∀ (m : ℕ) (hmn : m < n) (hg : m.gcd n = 1)
    (he : (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = (↑u : AddCircle p)),
    ∃ (a : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)),
      (fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
            (Subtype.mk (p := fun (x : AddCircle p) ↦
                Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
                (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
              { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
          a =
        u
⊢ ∃ (a : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)),
    (fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
          (Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
              (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
            { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
        a =
      u

Tactic:
obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2

Premises used: Iff.mp, AddCircle.addOrderOf_eq_pos_iff, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : (↑{u : AddCircle p | addOrderOf u = n} : Type u_1)
m : ℕ
hmn : m < n
hg : m.gcd n = 1
he : (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = (↑u : AddCircle p)
⊢ ∃ (a : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)),
    (fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
          (Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
              (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
            { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
        a =
      u

Tactic:
⟨⟨m, hmn, hg⟩, Subtype.ext he⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Subtype.ext
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : Field 𝕜
p q : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : (↑{u : AddCircle p | addOrderOf u = n} : Type u_1)
m : ℕ
hmn : m < n
hg : m.gcd n = 1
he : (↑(HDiv.hDiv (α := 𝕜) (↑m : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) = (↑u : AddCircle p)
⊢ ∃ (a : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)),
    (fun (m : (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type)) ↦
          (Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x)
              (↑(HDiv.hDiv (α := 𝕜) (↑(↑m : ℕ) : 𝕜) (↑n : 𝕜) * p) : 𝕜 ⧸ zmultiples p) ⋯ :
            { x : AddCircle p // Membership.mem (γ := Set (AddCircle p)) {u : AddCircle p | addOrderOf u = n} x }))
        a =
      u

Tactic:
exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
inl : Nat.card.{u_1} { u : AddCircle p // addOrderOf u = 0 } = Nat.totient 0
inr : ∀ (hn : n > 0), Nat.card.{u_1} { u : AddCircle p // addOrderOf u = n } = n.totient
⊢ Nat.card.{u_1} { u : AddCircle p // addOrderOf u = n } = n.totient

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
inl : Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0
⊢ Nat.card.{u_1} { u : AddCircle p // addOrderOf u = 0 } = Nat.totient 0

Tactic:
simp only [Nat.totient_zero, addOrderOf_eq_zero_iff]

Premises used: addOrderOf_eq_zero_iff, Nat.totient_zero
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
inl : ∀ (u : AddCircle p) (hu : ¬IsOfFinAddOrder u), Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0
inl₁ : ∀ (h : ¬∃ (u : AddCircle p), ¬IsOfFinAddOrder u), Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0
⊢ Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0

Tactic:
rcases em (∃ u : AddCircle p, ¬IsOfFinAddOrder u) with (⟨u, hu⟩ | h)

Premises used: Exists, em, IsOfFinAddOrder, Not
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
rw : Set.Infinite.{u_1} (α := AddCircle p) {x : AddCircle p | ¬IsOfFinAddOrder x}
⊢ Infinite.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }

Tactic:
rw [← coe_setOf, infinite_coe_iff]

Premises used: Set.infinite_coe_iff, Set.coe_setOf
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite.{u_1} (α := AddCircle p) {x : AddCircle p | ¬IsOfFinAddOrder x}

Tactic:
infinite_not_isOfFinAddOrder hu

Premises used: infinite_not_isOfFinAddOrder, setOf
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Set.Infinite.{u_1} (α := AddCircle p) {x : AddCircle p | ¬IsOfFinAddOrder x}

Tactic:
exact infinite_not_isOfFinAddOrder hu

Premises used: infinite_not_isOfFinAddOrder
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }

Tactic:
have : Infinite { u : AddCircle p // ¬IsOfFinAddOrder u } := by
        rw [← coe_setOf, infinite_coe_iff]
        exact infinite_not_isOfFinAddOrder hu
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }
⊢ Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0

Tactic:
Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
this : Infinite.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }
⊢ Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ (u : AddCircle p), ¬IsOfFinAddOrder u
⊢ IsEmpty.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }

Tactic:
simpa [isEmpty_subtype] using h

Premises used: isEmpty_subtype
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ (u : AddCircle p), ¬IsOfFinAddOrder u
⊢ IsEmpty.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }

Tactic:
have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa [isEmpty_subtype] using h
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ (u : AddCircle p), ¬IsOfFinAddOrder u
this : IsEmpty.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }
⊢ Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0

Tactic:
Nat.card_of_isEmpty

Premises used: Nat.card_of_isEmpty
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ (u : AddCircle p), ¬IsOfFinAddOrder u
this : IsEmpty.{max 1 (u_1 + 1)} { u : AddCircle p // ¬IsOfFinAddOrder u }
⊢ Nat.card.{u_1} { u : AddCircle p // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_of_isEmpty

Premises used: Nat.card_of_isEmpty
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
inr : Nat.card (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type) = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
⊢ Nat.card.{u_1} { u : AddCircle p // addOrderOf u = n } = n.totient

Tactic:
rw [← coe_setOf, Nat.card_congr (setAddOrderOfEquiv p hn),
      n.totient_eq_card_lt_and_coprime]

Premises used: Nat.card_congr, Set.coe_setOf, Nat.totient_eq_card_lt_and_coprime, AddCircle.setAddOrderOfEquiv
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card (↑{m : ℕ | m < n ∧ m.gcd n = 1} : Type) = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)

Tactic:
simp only [Nat.gcd_comm]

Premises used: Nat.gcd_comm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)
⊢ Eq.{u_1 + 1} (α := 𝕋)
    ((fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦
        ((↑(↑x : 𝕜) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
          HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
    ((fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦
        ((↑(↑x : 𝕜) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
          HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯))

Tactic:
(coe_add_period p a).symm

Premises used: AddCircle.coe_add_period, Eq.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)
⊢ Eq.{u_1 + 1} (α := 𝕋)
    ((fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦
        ((↑(↑x : 𝕜) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
          HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯))
    ((fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦
        ((↑(↑x : 𝕜) : HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) :
          HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯))

Tactic:
exact (coe_add_period p a).symm

Premises used: AddCircle.coe_add_period, Eq.symm
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
inl :
  ∀ (h : x ≠ a + p),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      ((fun (x : 𝕋) ↦
          (Quot.mk (EndpointIdent p a)
              (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
                ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
            Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
        ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
            x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
              ⋯)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
inr :
  ∀ (hx : a + p ∈ Icc a (a + p)),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      ((fun (x : 𝕋) ↦
          (Quot.mk (EndpointIdent p a)
              (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
                ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
            Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
        ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
            x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
              ⋯)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) hx))))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) hx))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    ((fun (x : 𝕋) ↦
        (Quot.mk (EndpointIdent p a)
            (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
              ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
          Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
      ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
          x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
            ⋯)
        (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))

Tactic:
rcases ne_or_eq x (a + p) with (h | rfl)

Premises used: ne_or_eq, HAdd.hAdd, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
inl :
  ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)) (h : x ≠ a + p),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      ((fun (x : 𝕋) ↦
          (Quot.mk (EndpointIdent p a)
              (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
                ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
            Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
        ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
            x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
              ⋯)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    ((fun (x : 𝕋) ↦
        (Quot.mk (EndpointIdent p a)
            (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
              ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
          Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
      ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
          x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
            ⋯)
        (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))

Tactic:
revert x
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inl :
  ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)) (h : x ≠ a + p),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.mk (EndpointIdent p a)
        (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
          ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1))
            (Quot.liftOn (r := EndpointIdent p a)
              (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
              (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) ⋯))))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)) (h : x ≠ a + p),
    Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      ((fun (x : 𝕋) ↦
          (Quot.mk (EndpointIdent p a)
              (Set.inclusion (s := Ico a (a + p)) (t := Icc a (a + p)) ⋯
                ((equivIco p a : (a_1 : 𝕋) → (↑(Ico a (a + p)) : Type u_1)) x)) :
            Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)))
        ((fun (x : Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a)) ↦
            x.liftOn (r := EndpointIdent p a) (fun (x : (↑(Icc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p))
              ⋯)
          (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))))
      (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) x hx))

Tactic:
dsimp only