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 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst_3 : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIcoMod (p := p) ⋯ a x) ⋯))
    (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯))
have pos : Eq (α := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
  (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) a sorry))
  (Quot.mk (EndpointIdent p a) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (a + p) sorry))
Tactic: simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 𝕜
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot]
    (Equiv.toFun (equivIccQuot p a))
have simp_rw : ∀ (x : 𝕜),
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
Tactic: simp_rw [isQuotientMap_quotient_mk'.continuous_iff, continuous_iff_continuousAt,
      continuousAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
have left : ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
  (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕜
left :
  ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x
⊢ ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
      (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
have right : ContinuousWithinAt (Y := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
  (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x
have left : 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)) (toIocMod (p := p) sorry a x) sorry))
  (Iic x) x
Tactic: erw [equivIccQuot_comp_mk_eq_toIocMod]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Iic x) x
have left : 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)) (toIocMod (p := p) sorry a x) sorry))
  (Iic x) x
Tactic: on_goal 1 => erw [equivIccQuot_comp_mk_eq_toIocMod]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
have right : 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) sorry a x) sorry))
  (Ici x) x
Tactic: erw [equivIccQuot_comp_mk_eq_toIcoMod]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := Quot (α := (↑(Icc a (a + p)) : Type u_1)) (EndpointIdent p a))
    (Equiv.toFun (equivIccQuot p a) ∘ Quotient.mk') (Ici x) x
have right : 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) sorry a x) sorry))
  (Ici x) x
Tactic: on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := 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)) (toIocMod (p := p) ⋯ a x) ⋯))
    (Iic x) x
have left : ContinuousWithinAt (Y := (↑(Icc a (a + p)) : Type u_1))
  (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) sorry a x) sorry) (Iic x) x
Tactic: apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := (↑(Icc a (a + p)) : Type u_1))
    (fun (x : 𝕜) ↦ Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ Icc a (a + p)) (toIocMod (p := p) ⋯ a x) ⋯) (Iic x) x
have left : 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) sorry a x) sorry)
  (Iic x) x
Tactic: rw [IsInducing.subtypeVal.continuousWithinAt_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := 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
have 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) sorry a x) sorry) (Ici x) x
Tactic: apply continuous_quot_mk.continuousAt.comp_continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 := (↑(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
have 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) sorry a x) sorry)
  (Ici x) x
Tactic: rw [IsInducing.subtypeVal.continuousWithinAt_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)
have h : ∀ (q : 𝕋), liftIoc p a f q = liftIco p a f q
Tactic: ext q
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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 : 𝕋
⊢ liftIoc p a f q = liftIco p a f q
have h : ∀ (x : 𝕜) (hx : x ∈ Ico a (a + p)), liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = liftIco p a f (↑x : 𝕜 ⧸ zmultiples p)
Tactic: obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = liftIco p a f (↑x : 𝕜 ⧸ zmultiples p)
have h : liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x
Tactic: rw [liftIco_coe_apply hx]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ a = x ∧ x < a + p ∨ a < x ∧ x < a + p
have rwa : ∀ (hx : 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
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ a = x ∧ x < a + p ∨ a < x ∧ x < a + p
have rwa₁ : ∀ (hx : (a = x ∨ 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
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ a = x ∧ x < a + p ∨ a < x ∧ x < a + p
have rwa₂ : ∀ (hx : 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
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x
have h : ∀ (hx : a ∈ Ico a (a + p)), liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a
Tactic: obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ liftIoc p a f (↑x : 𝕜 ⧸ zmultiples p) = f x
have h₁ : ∀ (h : a < x ∧ x < a + p), 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
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
⊢ liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a
have h : liftIoc p a f (↑(a + p) : 𝕜 ⧸ zmultiples p) = f a
Tactic: rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a
have h₁ : f (a + p) = f a
Tactic: rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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
⊢ liftIoc p a f (↑a : 𝕜 ⧸ zmultiples p) = f a
have h₂ : f (a + p) = f (a + p)
Tactic: rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)
    (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)))
have rw : Eq (α := 𝕋 → B) (liftIoc p a f) (liftIco p a f)
Tactic: rw [← liftIco_eq_lift_Icc h]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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] (liftIco p a f)
have 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) sorry)
    (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))
Tactic: rw [liftIco_eq_lift_Icc hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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)))
have refine : Continuous[instTopologicalSpaceQuot, inst_6]
  (Quot.lift (r := EndpointIdent p a) ((Icc a (a + p)).restrict (π := fun (a : 𝕜) ↦ B) f) sorry)
Tactic: refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.Defs (goal)
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] (liftIoc p a f)
have 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) sorry)
    (⇑(equivIccQuot p a) : (a_1 : 𝕋) → Quot (EndpointIdent p a)))
Tactic: rw [liftIoc_eq_lift_Icc hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
have inl : Dense (↑(AddSubgroup.closure {a, 0}) : Set ℝ) ↔ Irrational (a / 0)
Tactic: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
inl : Dense (↑(AddSubgroup.closure {a, 0}) : Set ℝ) ↔ Irrational (a / 0)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
have inr : ∀ (hb : b ≠ 0), Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
Tactic: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a : ℝ
⊢ Dense (↑(AddSubgroup.closure {a, 0}) : Set ℝ) ↔ Irrational (a / 0)
have inl : Dense (↑(AddSubgroup.closure {0, a}) : Set ℝ) ↔ Irrational (a / 0)
Tactic: rw [pair_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
have inr : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) → Irrational (a / b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
inr : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) → Irrational (a / b)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ) ↔ Irrational (a / b)
have inr₁ : Irrational (a / b) → Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ False
have inr : (↑(AddSubgroup.closure {a, b}) : Set ℝ) ⊆ range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))
Tactic: refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
hd : Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
r : ℚ
hr : (↑r : ℝ) = a / b
⊢ (↑(AddSubgroup.closure {a, b}) : Set ℝ) ⊆ range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))
have inr : Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) a ∧
  Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) b
Tactic: rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le,
      AddSubgroup.coe_zmultiples, pair_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
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
have inr : (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) r.num = a
Tactic: refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
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
⊢ Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) a ∧
    Membership.mem (γ := Set ℝ) (range fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) b
have inr₁ : (fun (x : ℤ) ↦ x • (b / (↑r.den : ℝ))) (↑r.den : ℤ) = b
Tactic: refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
h : Irrational (a / b)
⊢ Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
have inr : ∀ (h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)), ¬Irrational (a / b)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
⊢ ¬Irrational (a / b)
have inr : ∀ (c : ℝ) (hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})), ¬Irrational (a / b)
Tactic: rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
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)
have rw : {a, b} ⊆ (↑(AddSubgroup.closure {a, b}) : Set ℝ)
Tactic: rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (hypothesis)
Goal:
a b : ℝ
hb : b ≠ 0
h : ¬Dense (↑(AddSubgroup.closure {a, b}) : Set ℝ)
c : ℝ
hc : Eq (α := AddSubgroup ℝ) (AddSubgroup.closure {a, b}) (AddSubgroup.closure {c})
⊢ ¬Irrational (a / b)
have this : 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