awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 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)
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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
rw₁ rw₂ : n • p = n • p
⊢ n.toNat • p = n • p

Tactic:
rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]

Premises used: Int.toNat_of_nonneg, LT.lt.le, natCast_zsmul
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ (n_1 : ℕ), n_1 • p = n • p

Tactic:
exact ⟨n.toNat, by rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) p = n • p

Tactic:
simp
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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

Tactic:
exact ⟨(n : ℤ), by simp⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
rw₂ rw₃ :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    (↑(↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx) : 𝕜) : 𝕜 ⧸ zmultiples 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

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply, equivIco, QuotientAddGroup.equivIcoMod_symm_apply]

Premises used: AddCircle.equivIco, QuotientAddGroup.equivIcoMod_symm_apply, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
rw₂ rw₃ :
  Eq (α := AddCircle p) (↑x : 𝕜 ⧸ zmultiples p)
    (↑(↑(Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx) : 𝕜) : 𝕜 ⧸ zmultiples 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

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply, equivIoc, QuotientAddGroup.equivIocMod_symm_apply]

Premises used: AddCircle.equivIoc, QuotientAddGroup.equivIocMod_symm_apply, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
y : AddCircle p
⊢ (↑(↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) y) : 𝕜) : 𝕜 ⧸ zmultiples p) = y

Tactic:
(equivIco p a).left_inv y

Premises used: AddCircle.equivIco, Equiv.left_inv
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst_3 : Archimedean 𝕜
y : AddCircle p
⊢ (↑(↑((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) y) : 𝕜) : 𝕜 ⧸ zmultiples p) = y

Tactic:
(equivIoc p a).left_inv y

Premises used: AddCircle.equivIoc, Equiv.left_inv
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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) =
    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⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
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
⊢ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p)) : 𝕜) = y

Tactic:
simp [this]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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) =
    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⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
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
⊢ (↑((equivIoc p a : (a_1 : AddCircle p) → (↑(Ioc a (a + p)) : Type u_1)) (↑y : 𝕜 ⧸ zmultiples p)) : 𝕜) = y

Tactic:
simp [this]
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  x = y →
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ x = y →
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)

Tactic:
tauto
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
refine :
  ∀
    (h :
      Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
        (↑y : 𝕜 ⧸ zmultiples p)),
    x = y
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p) ↔
    x = y

Tactic:
refine ⟨fun h => ?_, by tauto⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
this : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
⊢ x = y

Tactic:
Subtype.mk.inj this

Premises used: Subtype.mk.inj
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
this : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ico a (a + p)) y hy
⊢ x = y

Tactic:
exact Subtype.mk.inj this

Premises used: Subtype.mk.inj
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
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
⊢ x = y

Tactic:
suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
⊢ 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

Premises used: AddCircle.equivIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
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)))
⊢ 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:
rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]

Premises used: AddCircle.equivIco, Equiv.right_inv, Subtype.mk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
⊢ 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:
h
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
⊢ 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:
exact h
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  x = y →
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)
⊢ x = y →
    Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p)

Tactic:
tauto
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
refine :
  ∀
    (h :
      Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p)
        (↑y : 𝕜 ⧸ zmultiples p)),
    x = y
⊢ Eq (α := HasQuotient.Quotient 𝕜 (B := AddSubgroup 𝕜) (zmultiples p)) (↑x : 𝕜 ⧸ zmultiples p) (↑y : 𝕜 ⧸ zmultiples p) ↔
    x = y

Tactic:
refine ⟨fun h => ?_, by tauto⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
this : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
⊢ x = y

Tactic:
Subtype.mk.inj this

Premises used: Subtype.mk.inj
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
this : Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) x hx = Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Ioc a (a + p)) y hy
⊢ x = y

Tactic:
exact Subtype.mk.inj this

Premises used: Subtype.mk.inj
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
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
⊢ x = y

Tactic:
suffices (⟨x, hx⟩ : Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
⊢ 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

Premises used: AddCircle.equivIoc
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
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)))
⊢ 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:
rw [← (equivIoc p a).right_inv ⟨x, hx⟩, ← (equivIoc p a).right_inv ⟨y, hy⟩]

Premises used: Equiv.right_inv, AddCircle.equivIoc, Subtype.mk
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
⊢ 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:
h
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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))
⊢ 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:
exact h
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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 : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIco p a f (↑x : 𝕜 ⧸ zmultiples p) = f x

Tactic:
simp [liftIco, equivIco_coe_eq hx]

Premises used: AddCircle.equivIco_coe_eq, AddCircle.liftIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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 : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x

Tactic:
simp [liftIoc, equivIoc_coe_eq hx]

Premises used: AddCircle.liftIoc, AddCircle.equivIoc_coe_eq
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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 = (↑(↑((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
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
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) : 𝕜)
⊢ liftIoc p a f x = liftIco p a f x

Tactic:
rw [x_eq_b, liftIco_coe_apply (equivIco p a x).coe_prop]

Premises used: AddCircle.equivIco, Subtype.coe_prop, AddCircle.liftIco_coe_apply, DFunLike.coe
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
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)
⊢ (↑((equivIco p a : (a_1 : AddCircle p) → (↑(Ico a (a + p)) : Type u_1)) x) : 𝕜) ∈ Ioc a (a + p)

Tactic:
grind
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
β : Type u_4
f : 𝕜 → α
g : α → β
a : 𝕜
x : AddCircle p
⊢ liftIco p a (g ∘ f) x = g (liftIco p a f x)

Tactic:
rfl

Premises used: Set.restrict, rfl, AddCircle.liftIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
α : Type u_3
β : Type u_4
f : 𝕜 → α
g : α → β
a : 𝕜
x : AddCircle p
⊢ liftIoc p a (g ∘ f) x = g (liftIoc p a f x)

Tactic:
rfl

Premises used: AddCircle.liftIoc, Set.restrict, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
a : AddCircle p
b : (↑(Ico 0 (0 + p)) : Type u_1) :=
  (QuotientAddGroup.equivIcoMod ⋯ 0 : (a : 𝕜 ⧸ zmultiples p) → (↑(Ico 0 (0 + p)) : Type u_1)) a
⊢ (↑b : 𝕜) ∈ Ico 0 p

Tactic:
simpa only [zero_add] using b.2

Premises used: zero_add, Subtype.property
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
a : AddCircle p
b : (↑(Ico 0 (0 + p)) : Type u_1) :=
  (QuotientAddGroup.equivIcoMod ⋯ 0 : (a : 𝕜 ⧸ zmultiples p) → (↑(Ico 0 (0 + p)) : Type u_1)) a
⊢ ∃ b ∈ Ico 0 p, (↑b : 𝕜 ⧸ zmultiples p) = a

Tactic:
exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
inst : AddCommGroup 𝕜
p : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
a : AddCircle p
b : (↑(Ioc 0 (0 + p)) : Type u_1) :=
  (QuotientAddGroup.equivIocMod ⋯ 0 : (a : 𝕜 ⧸ zmultiples p) → (↑(Ioc 0 (0 + p)) : Type u_1)) a
⊢ (↑b : 𝕜) ∈ Ioc 0 p

Tactic:
simpa only [zero_add] using b.2

Premises used: zero_add, Subtype.property