awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine_1 : IsOpen[inst_4] {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x}
⊢ toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a
have refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x} x
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst_4] {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x}
have refine_1 : IsOpen[inst_4] (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))
Tactic: rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x} x
have refine_2 : toIcoMod hp a x = toIocMod hp a x
Tactic: rwa [mem_setOf_eq, ← not_modEq_iff_toIcoMod_eq_toIocMod hp, AddCommGroup.modEq_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
refine_2 : toIcoMod hp a x = toIocMod hp a x
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (x : 𝕜) ↦ toIcoMod hp a x = toIocMod hp a x) x} x
have refine_2₁ : ¬a ≡ x [PMOD p]
Tactic: rwa [mem_setOf_eq, ← not_modEq_iff_toIcoMod_eq_toIocMod hp, AddCommGroup.modEq_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(x + p) : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)
have rw : HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
    (↑p : 𝕜 ⧸ zmultiples p) =
  (↑x : 𝕜 ⧸ zmultiples p)
Tactic: rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
rw :
  HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑p : 𝕜 ⧸ zmultiples p) =
    (↑x : 𝕜 ⧸ zmultiples p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(x + p) : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)
have rw₁ : (↑p : 𝕜 ⧸ zmultiples p) =
  HSub.hSub (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)
Tactic: rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
rw :
  HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑p : 𝕜 ⧸ zmultiples p) =
    (↑x : 𝕜 ⧸ zmultiples p)
rw₁ :
  (↑p : 𝕜 ⧸ zmultiples p) =
    HSub.hSub (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑x : 𝕜 ⧸ zmultiples p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(x + p) : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)
have rw₂ : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0
Tactic: rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p x : 𝕜
rw :
  HAdd.hAdd (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑p : 𝕜 ⧸ zmultiples p) =
    (↑x : 𝕜 ⧸ zmultiples p)
rw₁ :
  (↑p : 𝕜 ⧸ zmultiples p) =
    HSub.hSub (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑x : 𝕜 ⧸ zmultiples p)
rw₂ : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑p : 𝕜 ⧸ zmultiples p) 0
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑(x + p) : 𝕜 ⧸ zmultiples p)
    (↑x : 𝕜 ⧸ zmultiples p)
have rw₃ : Eq.{u_1 + 1} (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) 0 0
Tactic: rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
x : (↑{x : AddCircle p | n • x = 0} : Type u_1)
⊢ ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p
have obtain : ∀ (x : AddCircle p) (hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x),
  ∃ (k : Fin n) (y : 𝕜),
    (↑y : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) x hx) :
          AddCircle p) ∧
      n • y = (↑k : ℕ) • p
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
x : AddCircle p
hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x
⊢ ∃ (k : Fin n) (y : 𝕜),
    (↑y : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) x hx) :
          AddCircle p) ∧
      n • y = (↑k : ℕ) • p
have obtain : ∀ (y : 𝕜) (hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)),
  ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
Tactic: obtain ⟨y, rfl⟩ := mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
have hx₁ : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
Tactic: rw [Set.mem_setOf, ← mk_nsmul, eq_zero_iff] at hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
have have : ∀ (m' : ℤ) (hm : (fun (x : ℤ) ↦ x • p) m' = n • y),
  ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
Tactic: have ⟨m', hm⟩ := hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
hm : (fun (x : ℤ) ↦ x • p) m' = n • y
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
have this : NeZero n
Tactic: have : NeZero n := ⟨h0⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
hm : (fun (x : ℤ) ↦ x • p) m' = n • y
this : NeZero n
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
have hm₁ : (fun (x : ℤ) ↦ x • p)
    (HMul.hMul (α := ℤ) ((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').1 (↑n : ℤ) +
      (↑(↑((Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m').2 : ℕ) : ℤ)) =
  n • y
Tactic: rw [← (Int.divModEquiv n).symm_apply_apply m', Int.divModEquiv_symm_apply] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
⊢ ∃ (k : Fin n) (y_1 : 𝕜),
    (↑y_1 : 𝕜 ⧸ zmultiples p) =
        (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
              Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
          AddCircle p) ∧
      n • y_1 = (↑k : ℕ) • p
have h : (↑(y - m.1 • p) : 𝕜 ⧸ zmultiples p) =
    (↑(Subtype.mk (p := fun (x : AddCircle p) ↦ Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x)
          (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
      AddCircle p) ∧
  n • (y - m.1 • p) = (↑m.2 : ℕ) • p
Tactic: use m.2, y - m.1 • p
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
⊢ (↑(y - m.1 • p) : 𝕜 ⧸ zmultiples p) =
      (↑(Subtype.mk (p := fun (x : AddCircle p) ↦
            Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} x) (↑y : 𝕜 ⧸ zmultiples p) hx_1) :
        AddCircle p) ∧
    n • (y - m.1 • p) = (↑m.2 : ℕ) • p
have h : True ∧ n • (y - m.1 • p) = (↑m.2 : ℕ) • p
Tactic: simp_rw [mk_sub, mk_zsmul, sub_eq_self, coe_period, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx_1 : Membership.mem (γ := Set (AddCircle p)) {x : AddCircle p | n • x = 0} (↑y : 𝕜 ⧸ zmultiples p)
hx : Membership.mem (γ := AddSubgroup 𝕜) (zmultiples p) (n • y)
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n : (a : ℤ) → ℤ × Fin n) m'
hm : (fun (x : ℤ) ↦ x • p) (m.1 * (↑n : ℤ) + (↑(↑m.2 : ℕ) : ℤ)) = n • y
⊢ True ∧ n • (y - m.1 • p) = (↑m.2 : ℕ) • p
have h : True ∧ (fun (x : ℤ) ↦ x • p) ((↑(↑m.2 : ℕ) : ℤ) + m.1 * (↑n : ℤ)) = (↑m.2 : ℕ) • p + n • m.1 • p
Tactic: rw [smul_sub, sub_eq_iff_eq_add, ← hm, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)
have this : ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
  ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p
Tactic: have (x : {x : AddCircle p | n • x = 0}) : ∃ (k : Fin n) (y : 𝕜), y = x.1 ∧ n • y = k.1 • p := by
    obtain ⟨x, hx⟩ := x
    obtain ⟨y, rfl⟩ := mk_surjective x
    rw [Set.mem_setOf, ← mk_nsmul, eq_zero_iff] at hx
    have ⟨m', hm⟩ := hx
    have : NeZero n := ⟨h0⟩
    rw [← (Int.divModEquiv n).symm_apply_apply m', Int.divModEquiv_symm_apply] at hm
    set m := m'.divModEquiv n
    use m.2, y - m.1 • p
    simp_rw [mk_sub, mk_zsmul, sub_eq_self, coe_period, smul_zero]
    rw [smul_sub, sub_eq_iff_eq_add, ← hm, add_comm]
    simp [add_smul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
this :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (k : Fin n) (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑k : ℕ) • p
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)
have choose : ∀ (f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n)
  (hf :
    ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
      ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p),
  encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)
Tactic: choose f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n : ℕ∞)
have refine : ∀ (x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)) (eq : f x = f x'), (↑x : AddCircle p) = (↑x' : AddCircle p)
Tactic: refine (ENat.card_le_card_of_injective (f := f) fun x x' eq ↦ Subtype.ext ?_).trans (by simp)
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)
have have : ∀ (y : 𝕜) (hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)) (hy : n • y = (↑(f x) : ℕ) • p),
  (↑x : AddCircle p) = (↑x' : AddCircle p)
Tactic: have ⟨y, hyx, hy⟩ := hf x
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
hy : n • y = (↑(f x) : ℕ) • p
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)
have have : ∀ (y' : 𝕜) (hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)) (hy' : n • y' = (↑(f x') : ℕ) • p),
  (↑x : AddCircle p) = (↑x' : AddCircle p)
Tactic: have ⟨y', hyx', hy'⟩ := hf x'
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
hy : n • y = (↑(f x) : ℕ) • p
y' : 𝕜
hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
hy' : n • y' = (↑(f x') : ℕ) • p
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)
have rw : ∀ (y' : 𝕜) (hy : y = y') (hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)) (hy' : n • y' = (↑(f x') : ℕ) • p),
  (↑x : AddCircle p) = (↑x' : AddCircle p)
Tactic: rw [eq, ← hy', hn.eq_iff] at hy
Cleared hypotheses: hy, y', hyx', hy'
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
y' : 𝕜
hy : y = y'
hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
hy' : n • y' = (↑(f x') : ℕ) • p
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)
have rw : (↑y : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
Tactic: rw [← hyx, hy, hyx']
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
f : (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)) → Fin n
hf :
  ∀ (x : (↑{x : AddCircle p | n • x = 0} : Type u_1)),
    ∃ (y : 𝕜), (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p) ∧ n • y = (↑(f x) : ℕ) • p
x x' : (↑{x : AddCircle p | n • x = 0} : Type u_1)
eq : f x = f x'
y : 𝕜
hyx : (↑y : 𝕜 ⧸ zmultiples p) = (↑x : AddCircle p)
y' : 𝕜
hy : y = y'
hyx' : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
hy' : n • y' = (↑(f x') : ℕ) • p
rw : (↑y : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
rw₁ : (↑y' : 𝕜 ⧸ zmultiples p) = (↑x' : AddCircle p)
⊢ (↑x : AddCircle p) = (↑x' : AddCircle p)
have rw₂ : (↑x' : AddCircle p) = (↑x' : AddCircle p)
Tactic: rw [← hyx, hy, hyx']
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have a : Nontrivial 𝕜
Tactic: nontriviality 𝕜
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have inl : ∀ (hn : IsSMulRegular (R := ℕ) 𝕜 0),
  Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℕ) 0 x = 0}
Tactic: obtain rfl | h0 := eq_or_ne n 0
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
inl :
  ∀ (hn : IsSMulRegular (R := ℕ) 𝕜 0),
    Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℕ) 0 x = 0}
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have inr : ∀ (h0 : n ≠ 0), Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
Tactic: obtain rfl | h0 := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} ≤ (↑n.natAbs : ℕ∞)
have h : encard.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0} =
  encard.{u_1} (α := AddCircle p) {x : AddCircle p | n.natAbs • x = 0}
Tactic: convert!
    card_torsion_le_of_isSMulRegular p _ (Int.natAbs_ne_zero.mpr h0)
      (IsSMulRegular.natAbs_iff.mpr hn) using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have a : Nontrivial 𝕜
Tactic: nontriviality 𝕜
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have inl : ∀ (hn : IsSMulRegular (R := ℤ) 𝕜 0),
  Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℤ) 0 x = 0}
Tactic: obtain rfl | h0 := eq_or_ne n 0
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
h : Nontrivial 𝕜
inl :
  ∀ (hn : IsSMulRegular (R := ℤ) 𝕜 0),
    Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | HSMul.hSMul (α := ℤ) 0 x = 0}
⊢ Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
have inr : ∀ (h0 : n ≠ 0), Set.Finite.{u_1} (α := AddCircle p) {x : AddCircle p | n • x = 0}
Tactic: obtain rfl | h0 := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) 0 ↔ ∃ (n : ℕ), n • p = x
have rw : (∃ (n : ℤ), n • p = x) ↔ ∃ (n : ℕ), n • p = x
Tactic: rw [coe_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ (n : ℤ), n • p = x) ↔ ∃ (n : ℕ), n • p = x
have mp : (∃ (n : ℤ), n • p = x) → ∃ (n : ℕ), n • p = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
mp : (∃ (n : ℤ), n • p = x) → ∃ (n : ℕ), n • p = x
⊢ (∃ (n : ℤ), n • p = x) ↔ ∃ (n : ℕ), n • p = x
have mpr : (∃ (n : ℕ), n • p = x) → ∃ (n : ℤ), n • p = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n
have contrapose! : ∀ (hx : n ≤ 0), n • p ≤ 0
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ (n_1 : ℕ), n_1 • p = n • p
have hx₁ : 0 < n
Tactic: replace hx : 0 < n := by
      contrapose! hx
      simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ n.toNat • p = n • p
have rw : HSMul.hSMul (α := ℤ) (↑n.toNat : ℤ) p = n • p
Tactic: rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
rw : HSMul.hSMul (α := ℤ) (↑n.toNat : ℤ) p = n • p
⊢ n.toNat • p = n • p
have rw₁ : n • p = n • p
Tactic: rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]