awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ (equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx
have rw : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  ((Equiv.symm (equivIco p a) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx))
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIco, QuotientAddGroup.equivIcoMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
rw :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (equivIco p a) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx))
⊢ (equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx
have rw₁ : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  ((Equiv.symm (QuotientAddGroup.equivIcoMod sorry a) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx))
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIco, QuotientAddGroup.equivIcoMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
rw :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (equivIco p a) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx))
rw₁ :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (QuotientAddGroup.equivIcoMod ⋯ a) : (a : (↑(Ico a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx))
⊢ (equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx
have rw₂ : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  (↑(↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx) : 𝕜) : 𝕜 ⧸ zmultiples p)
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIco, QuotientAddGroup.equivIcoMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ (equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx
have rw : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  ((Equiv.symm (equivIoc p a) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx))
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ioc a (a + p)
rw :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (equivIoc p a) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx))
⊢ (equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx
have rw₁ : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  ((Equiv.symm (QuotientAddGroup.equivIocMod sorry a) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)
    (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx))
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ioc a (a + p)
rw :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (equivIoc p a) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx))
rw₁ :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    ((Equiv.symm (QuotientAddGroup.equivIocMod ⋯ a) : (a : (↑(Ioc a (a + p)) : Type u_1)) → AddCircle p)
      (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx))
⊢ (equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) =
    Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx
have rw₂ : Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
  (↑(↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx) : 𝕜) : 𝕜 ⧸ zmultiples p)
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ico a (a + p)
⊢ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p)) : 𝕜) = y
have this : (equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) =
  Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
Tactic: have : equivIco p a y = ⟨y, hy⟩ := (equivIco p a).right_inv ⟨y, hy⟩
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ioc a (a + p)
⊢ (↑((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p)) : 𝕜) = y
have this : (equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) =
  Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
Tactic: have : equivIoc p a y = ⟨y, hy⟩ := (equivIoc p a).right_inv ⟨y, hy⟩
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p) ↔
    x = y
have refine : ∀
  (h :
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑y : 𝕜 ⧸ zmultiples p)),
  x = y
Tactic: refine ⟨fun h => ?_, by tauto⟩
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ x = y
have suffices : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
Tactic: suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
have h₁ : Eq (α := (↑(Ico a (a + p)) : Type u_1))
  ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) :
    (↑(Ico a (a + p)) : Type u_1))
  ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) :
    (↑(Ico a (a + p)) : Type u_1))
Tactic: apply_fun equivIco p a at h
Cleared hypotheses: h
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h :
  Eq (α := (↑(Ico a (a + p)) : Type u_1))
    ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) :
      (↑(Ico a (a + p)) : Type u_1))
    ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) :
      (↑(Ico a (a + p)) : Type u_1))
⊢ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
have rw : Eq (α := { x : 𝕜 // x ∈ Ico a (a + p) })
  (Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx)))
  (Equiv.toFun (equivIco p a) (Equiv.invFun (equivIco p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy)))
Tactic: rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p) ↔
    x = y
have refine : ∀
  (h :
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
      (↑y : 𝕜 ⧸ zmultiples p)),
  x = y
Tactic: refine ⟨fun h => ?_, by tauto⟩
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ x = y
have suffices : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
Tactic: suffices (⟨x, hx⟩ : Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
have h₁ : Eq (α := (↑(Ioc a (a + p)) : Type u_1))
  ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) :
    (↑(Ioc a (a + p)) : Type u_1))
  ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) :
    (↑(Ioc a (a + p)) : Type u_1))
Tactic: apply_fun equivIoc p a at h
Cleared hypotheses: h
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h :
  Eq (α := (↑(Ioc a (a + p)) : Type u_1))
    ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑x : 𝕜 ⧸ zmultiples p) :
      (↑(Ioc a (a + p)) : Type u_1))
    ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p) :
      (↑(Ioc a (a + p)) : Type u_1))
⊢ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
have rw : Eq (α := { x : 𝕜 // x ∈ Ioc a (a + p) })
  (Equiv.toFun (equivIoc p a) (Equiv.invFun (equivIoc p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx)))
  (Equiv.toFun (equivIoc p a) (Equiv.invFun (equivIoc p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy)))
Tactic: rw [← (equivIoc p a).right_inv ⟨x, hx⟩, ← (equivIoc p a).right_inv ⟨y, hy⟩]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
⊢ liftIoc p a f x = liftIco p a f x
have x_eq_b : x = (↑(↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) : 𝕜 ⧸ zmultiples p)
Tactic: have x_eq_b : x = ↑(equivIco p a x) := coe_equivIco.symm
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
x_eq_b : x = (↑(↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) : 𝕜 ⧸ zmultiples p)
⊢ liftIoc p a f x = liftIco p a f x
have rw : liftIoc p a f (↑(↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) : 𝕜 ⧸ zmultiples p) =
  f (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜)
Tactic: rw [x_eq_b, liftIco_coe_apply (equivIco p a x).coe_prop]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔ a = 0
have h0 : 0 ∈ Ico 0 (0 + p)
Tactic: have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔ a = 0
have ha' : a ∈ Ico 0 (0 + p)
Tactic: have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔ a = 0
have rw : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) (↑0 : 𝕜 ⧸ zmultiples p)
Tactic: rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
rw :
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) (↑0 : 𝕜 ⧸ zmultiples p)
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔ a = 0
have rw₁ : Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0 ↔
  Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑a : 𝕜 ⧸ zmultiples p) 0
Tactic: rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (Y := (↑(Ico a (a + p)) : Type u_1))
    (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x
have H : ∀ (z : 𝕜) (hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)),
  ContinuousAt (X := AddCircle p) (Y := (↑(Ico a (a + p)) : Type u_1))
    (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
Tactic: induction x using QuotientAddGroup.induction_on
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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (X := AddCircle p) (Y := (↑(Ico a (a + p)) : Type u_1))
    (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
have H : LE.le (α := Filter (↑(Ico a (a + p)) : Type u_1))
  (Filter.map
      (comp (β := AddCircle p) (⇑(equivIco p a) : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1))
        QuotientAddGroup.mk)
      (𝓝 z) :
    Filter (↑(Ico a (a + p)) : Type u_1))
  (𝓝 ((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
    Filter (↑(Ico a (a + p)) : Type u_1))
Tactic: rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ (↑a : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (Y := (↑(Ioc a (a + p)) : Type u_1))
    (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) x
have H : ∀ (z : 𝕜) (hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)),
  ContinuousAt (X := AddCircle p) (Y := (↑(Ioc a (a + p)) : Type u_1))
    (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
Tactic: induction x using QuotientAddGroup.induction_on
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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : AddCircle p
z : 𝕜
hx : Ne (α := AddCircle p) (↑z : 𝕜 ⧸ zmultiples p) (↑a : 𝕜 ⧸ zmultiples p)
⊢ ContinuousAt (X := AddCircle p) (Y := (↑(Ioc a (a + p)) : Type u_1))
    (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)
have H : LE.le (α := Filter (↑(Ioc a (a + p)) : Type u_1))
  (Filter.map
      (comp (β := AddCircle p) (⇑(equivIoc p a) : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1))
        QuotientAddGroup.mk)
      (𝓝 z) :
    Filter (↑(Ioc a (a + p)) : Type u_1))
  (𝓝 ((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑z : 𝕜 ⧸ zmultiples p)) :
    Filter (↑(Ioc a (a + p)) : Type u_1))
Tactic: rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))) (QuotientAddGroup.mk '' Ico a (a + p)) univ
have rw : Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
  (range fun (x : (↑(Ico a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ
Tactic: rw [image_eq_range]
-- 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 : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
⊢ Eq (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p))) (QuotientAddGroup.mk '' Ioc a (a + p)) univ
have rw : Eq.{u_1 + 1} (α := Set (HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)))
  (range fun (x : (↑(Ioc a (a + p)) : Type u_1)) ↦ (↑(↑x : 𝕜) : 𝕜 ⧸ zmultiples p)) univ
Tactic: rw [image_eq_range]
-- 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 : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
⊢ f = g
have rw : EqOn f g (QuotientAddGroup.mk '' Ico a (a + p))
Tactic: rw [← Set.eqOn_univ, ← coe_image_Ico_eq p a]
-- 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 : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f (↑x : 𝕜 ⧸ zmultiples p) = g (↑x : 𝕜 ⧸ zmultiples p)
⊢ f = g
have rw : EqOn f g (QuotientAddGroup.mk '' Ioc a (a + p))
Tactic: rw [← Set.eqOn_univ, ← coe_image_Ioc_eq p a]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q r : 𝕜
m : ℕ
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have rw : (↑((↑m : 𝕜) * (r / q)) : 𝕜 ⧸ zmultiples p) =
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
Tactic: rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
p q r : 𝕜
m : ℕ
rw :
  (↑((↑m : 𝕜) * (r / q)) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
⊢ (↑((↑m : 𝕜) / q * r) : 𝕜 ⧸ zmultiples p) =
    HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
have rw₁ : (↑(m • (r / q)) : 𝕜 ⧸ zmultiples p) =
  HSMul.hSMul (β := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) m (↑(r / q) : 𝕜 ⧸ zmultiples p)
Tactic: rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]