awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
right :
  ContinuousWithinAt (Y := (↑(Icc a (a + p)) : Type u_1))
    (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯) (Ici x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (fun (x : 𝕜) ↦
      Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Ici x) x

Tactic:
apply continuous_quot_mk.continuousAt.comp_continuousWithinAt

Premises used: Continuous.continuousAt, continuous_quot_mk, ContinuousAt.comp_continuousWithinAt
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
right :
  ContinuousWithinAt (Y := 𝕜)
    (comp (β := { x : 𝕜 // x ∈ Icc a (a + p) }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p))) fun (x : 𝕜) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯)
    (Ici x) x
⊢ ContinuousWithinAt (Y := (↑(Icc a (a + p)) : Type u_1))
    (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯) (Ici x) x

Tactic:
rw [IsInducing.subtypeVal.continuousWithinAt_iff]

Premises used: Topology.IsInducing.continuousWithinAt_iff, Topology.IsInducing.subtypeVal
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Y := 𝕜)
    (comp (β := { x : 𝕜 // x ∈ Icc a (a + p) }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p))) fun (x : 𝕜) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯)
    (Iic x) x

Tactic:
apply continuousWithinAt_toIocMod_Iic

Premises used: continuousWithinAt_toIocMod_Iic
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Y := 𝕜)
    (comp (β := { x : 𝕜 // x ∈ Icc a (a + p) }) (Subtype.val (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p))) fun (x : 𝕜) ↦
      Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯)
    (Ici x) x

Tactic:
apply continuousWithinAt_toIcoMod_Ici

Premises used: continuousWithinAt_toIcoMod_Ici
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
h : ∀ (q : 𝕋), liftIoc p a f q = liftIco p a f q
⊢ Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)

Tactic:
ext q
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
q : 𝕋
⊢ Membership.mem (γ := Set 𝕋) (QuotientAddGroup.mk '' Ico a (a + p)) q

Tactic:
simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q

Premises used: Set.mem_image
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
q : 𝕋
h : ∀ (x : 𝕜) (hx : x ∈ Ico a (a + p)), liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = liftIco p a f (↑x : 𝕜 ⧸ zmultiples p)
⊢ liftIoc p a f q = liftIco p a f q

Tactic:
obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q

Premises used: 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = liftIco p a f (↑x : 𝕜 ⧸ zmultiples p)

Tactic:
rw [liftIco_coe_apply hx]

Premises used: AddCircle.liftIco_coe_apply
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
rwa : ∀ (hx : a ≤ x ∧ x < a + p), a = x ∧ x < a + p ∨ a < x ∧ x < a + p
rwa₁ : ∀ (hx : (a = x ∨ a < x) ∧ x < a + p), a = x ∧ x < a + p ∨ a < x ∧ x < a + p
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hx : a = x ∧ x < a + p ∨ a < x ∧ x < a + p), a = x ∧ x < a + p ∨ a < x ∧ x < a + p
⊢ a = x ∧ x < a + p ∨ a < x ∧ x < a + p

Tactic:
rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx

Premises used: le_iff_eq_or_lt, Set.mem_Ico, or_and_right
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : ∀ (hx : a ∈ Ico a (a + p)), liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a
h₁ : ∀ (h : a < x ∧ x < a + p), liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x

Tactic:
obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx

Premises used: 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
hx : a ∈ Ico a (a + p)
⊢ a + p ∈ Ioc a (a + p)

Tactic:
simp [hp.out]

Premises used: Fact.out
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
hx : a ∈ Ico a (a + p)
h : liftIoc p a f (↑(a + p) : 𝕜 ⧸ zmultiples p) = f a
h₁ : f (a + p) = f a
h₂ h₃ : f (a + p) = f (a + p)
⊢ liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a

Tactic:
rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]

Premises used: AddCircle.coe_add_period, AddCircle.liftIoc_coe_apply
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : a < x ∧ x < a + p
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x

Tactic:
liftIoc_coe_apply ⟨h.1, h.2.le⟩

Premises used: LT.lt.le, AddCircle.liftIoc_coe_apply, And.right, And.left, And.intro
-- 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 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
h : a < x ∧ x < a + p
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x

Tactic:
exact liftIoc_coe_apply ⟨h.1, h.2.le⟩

Premises used: LT.lt.le, AddCircle.liftIoc_coe_apply, And.right, And.left, And.intro
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ (Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯) =
    (Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯)

Tactic:
h

Premises used: Set.restrict
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ (Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a ⋯) =
    (Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) ⋯)

Tactic:
exact h
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ Eq (α := 𝕋 → B) (liftIco p a f)
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))

Tactic:
rfl

Premises used: Quotient.liftOn', setOf, Function.Periodic.lift, Set.Icc, Set.restrict, rfl, AddCircle.liftIco
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
rw : Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)
⊢ Eq (α := 𝕋 → B) (liftIoc p a f)
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))

Tactic:
rw [← liftIco_eq_lift_Icc h]

Premises used: AddCircle.liftIco_eq_lift_Icc
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)

Tactic:
liftIoc_eq_liftIco h

Premises used: AddCircle.liftIoc_eq_liftIco
-- 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 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)

Tactic:
exact liftIoc_eq_liftIco h

Premises used: AddCircle.liftIoc_eq_liftIco
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ Ioc 0 p
⊢ x ∈ Ioc 0 (0 + p)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
rw :
  Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6]
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6] (liftIco p a f)

Tactic:
rw [liftIco_eq_lift_Icc hf]

Premises used: AddCircle.liftIco_eq_lift_Icc
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6]
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))

Tactic:
Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun

Premises used: Continuous.comp, Homeomorph.continuous_toFun, AddCircle.homeoIccQuot
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
refine :
  Continuous[instTopologicalSpaceQuot, inst_6]
    (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6]
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))

Tactic:
refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun

Premises used: Continuous.comp, Homeomorph.continuous_toFun, AddCircle.homeoIccQuot
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[instTopologicalSpaceQuot, inst_6]
    (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)

Tactic:
continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)

Premises used: Iff.mpr, continuous_coinduced_dom, continuousOn_iff_continuous_restrict, Iff.mp
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[instTopologicalSpaceQuot, inst_6]
    (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)

Tactic:
exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)

Premises used: Iff.mpr, continuous_coinduced_dom, continuousOn_iff_continuous_restrict, Iff.mp
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
rwa rwa₁ rwa₂ rwa₃ : f 0 = f p
⊢ f 0 = f (0 + p)

Tactic:
rwa [zero_add]

Premises used: zero_add
-- Module: Mathlib.Topology.Instances.AddCircle.Defs
Goal:
𝕜 : Type u_1
B : Type u_2
inst : AddCommGroup 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))

Tactic:
rwa [zero_add]

Premises used: zero_add
-- 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 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
rw :
  Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6]
    (comp (β := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) ⋯)
      (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst_6] (liftIoc p a f)

Tactic:
rw [liftIoc_eq_lift_Icc hf]

Premises used: AddCircle.liftIoc_eq_lift_Icc
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
inl : Dense (↑(AddSubgroup.closure {a, 0}) : Set ℝ) ↔ Irrational (a / 0)
inr : ∀ (hb : b ≠ 0), Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a : ℝ
inl : Dense (↑(AddSubgroup.closure {0, a}) : Set ℝ) ↔ Irrational (a / 0)
⊢ Dense (↑(AddSubgroup.closure {a, 0}) : Set ℝ) ↔ Irrational (a / 0)

Tactic:
rw [pair_comm]

Premises used: Set.pair_comm
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a : ℝ
⊢ Dense (↑(AddSubgroup.closure {0, a}) : Set ℝ) ↔ Irrational (a / 0)

Tactic:
simpa [← AddSubgroup.zmultiples_eq_closure] using not_denseRange_zsmul

Premises used: AddSubgroup.zmultiples_eq_closure, not_denseRange_zsmul
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
inr : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) → Irrational (a / b)
inr₁ : Irrational (a / b) → Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ False

Tactic:
not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_

Premises used: Dense.mono, not_denseRange_zsmul
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
inr : (↑(AddSubgroup.closure {a, b}) : Set ℝ) ⊆ range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))
⊢ False

Tactic:
refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_

Premises used: Dense.mono, not_denseRange_zsmul
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
inr :
  Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) a ∧
    Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) b
⊢ (↑(AddSubgroup.closure {a, b}) : Set ℝ) ⊆ range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))

Tactic:
rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]

Premises used: AddSubgroup.coe_zmultiples, Set.pair_subset_iff, SetLike.coe_subset_coe, AddSubgroup.closure_le
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) a ∧
    Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) b

Tactic:
⟨⟨r.num, ?_⟩, r.den, ?_⟩

Premises used: Rat.num, Rat.den, Nat.cast, And.intro, Exists.intro
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
inr : (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) r.num = a
inr₁ : (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) (↑r.den : ℤ) = b
⊢ Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) a ∧
    Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) b

Tactic:
refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) r.num = a

Tactic:
simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]

Premises used: Rat.cast_def, mul_div_left_comm
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) (↑r.den : ℤ) = b

Tactic:
simp [field]
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : Irrational (a / b)
inr : ∀ (h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)), ¬Irrational (a / b)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)

Tactic:
contrapose h
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
inr :
  ∀ (c : ℝ) (hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})), ¬Irrational (a / b)
⊢ ¬Irrational (a / b)

Tactic:
rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩

Premises used: Or.resolve_left, AddSubgroup.dense_or_cyclic
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
c : ℝ
hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})
rw : {a, b} ⊆ (↑(AddSubgroup.closure {a, b}) : Set ℝ)
⊢ Subset (α := Set ℝ) {a, b} (range fun (x : ℤ) ↦ x • c)

Tactic:
rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]

Premises used: AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
c : ℝ
hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})
⊢ {a, b} ⊆ (↑(AddSubgroup.closure {a, b}) : Set ℝ)

Tactic:
apply AddSubgroup.subset_closure

Premises used: AddSubgroup.subset_closure
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
c : ℝ
hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})
⊢ Subset (α := Set ℝ) {a, b} (range fun (x : ℤ) ↦ x • c)

Tactic:
have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by
      rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
      apply AddSubgroup.subset_closure
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
c : ℝ
hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})
this : Subset (α := Set ℝ) {a, b} (range fun (x : ℤ) ↦ x • c)
inr :
  ∀ (m n : ℤ) (hb : Ne (α := ℝ) ((fun (x : ℤ) ↦ x • c) n) 0)
    (h : ¬Dense (↑(AddSubgroup.closure {(fun (x : ℤ) ↦ x • c) m, (fun (x : ℤ) ↦ x • c) n}) : Set ℝ))
    (hc :
      Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {(fun (x : ℤ) ↦ x • c) m, (fun (x : ℤ) ↦ x • c) n})
        (AddSubgroup.closure {c}))
    (this : Subset (α := Set ℝ) {(fun (x : ℤ) ↦ x • c) m, (fun (x : ℤ) ↦ x • c) n} (range fun (x : ℤ) ↦ x • c)),
    ¬Irrational (HDiv.hDiv (α := ℝ) ((fun (x : ℤ) ↦ x • c) m) ((fun (x : ℤ) ↦ x • c) n))
⊢ ¬Irrational (a / b)

Tactic:
rcases pair_subset_iff.1 this with ⟨⟨m, rfl⟩, n, rfl⟩

Premises used: Set.pair_subset_iff, Iff.mp, rfl