awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
c : ℝ
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))

Tactic:
simp_all [mul_div_mul_right]

Premises used: mul_div_mul_right
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
rcases :
  ∀ (a : ℝ),
    (DenseRange (X := AddCircle p) fun (x : ℤ) ↦ HSMul.hSMul (β := AddCircle p) x (↑a : ℝ ⧸ AddSubgroup.zmultiples p)) ↔
      addOrderOf (G := AddCircle p) (↑a : ℝ ⧸ AddSubgroup.zmultiples p) = 0
⊢ (DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a) ↔ addOrderOf a = 0

Tactic:
rcases QuotientAddGroup.mk_surjective a with ⟨a, rfl⟩

Premises used: QuotientAddGroup.mk_surjective, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : ℝ
⊢ (DenseRange (X := AddCircle p) fun (x : ℤ) ↦ HSMul.hSMul (β := AddCircle p) x (↑a : ℝ ⧸ AddSubgroup.zmultiples p)) ↔
    addOrderOf (G := AddCircle p) (↑a : ℝ ⧸ AddSubgroup.zmultiples p) = 0

Tactic:
simp [denseRange_zsmul_coe_iff, isOfFinAddOrder_iff_exists_rat_eq_div, Irrational]

Premises used: AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div, AddCircle.denseRange_zsmul_coe_iff, Irrational
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
mp : Dense (↑s : Set (AddCircle p)) → ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a
mpr : (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense (↑s : Set (AddCircle p))
⊢ Dense (↑s : Set (AddCircle p)) ↔ ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : Dense (↑(AddSubgroup.zmultiples a) : Set (AddCircle p))
⊢ addOrderOf a = 0

Tactic:
rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd

Premises used: AddSubgroup.coe_zmultiples, AddCircle.denseRange_zsmul_iff, DenseRange
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False

Tactic:
ha hd
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False

Tactic:
exact ha hd
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a
mpr : ∀ (h : ¬Dense (↑s : Set (AddCircle p))), ∃ (a : AddCircle p), addOrderOf a ≠ 0 ∧ s = AddSubgroup.zmultiples a
⊢ Dense (↑s : Set (AddCircle p))

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense (↑s : Set (AddCircle p))
⊢ ∃ (a : ℝ), AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a

Tactic:
rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h

Premises used: AddSubgroup.coe_comap, QuotientAddGroup.coe_mk', AddSubgroup.dense_xor_cyclic, QuotientAddGroup.dense_preimage_mk, Iff.mp, xor_iff_not_iff'
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∃ (a : ℝ), AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
rcases :
  ∀ (a : ℝ) (ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a),
    ∃ (a : AddCircle p), s = AddSubgroup.zmultiples a
⊢ ∃ (a : AddCircle p), s = AddSubgroup.zmultiples a

Tactic:
rcases h with ⟨a, ha⟩
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
h : s = AddSubgroup.zmultiples (↑a : ℝ ⧸ AddSubgroup.zmultiples p)
⊢ ∃ (a : AddCircle p), s = AddSubgroup.zmultiples a

Tactic:
use a
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
h :
  Function.Surjective (α := ℝ) (β := AddCircle p)
    (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : ℝ) → AddCircle p)
⊢ s = AddSubgroup.zmultiples (↑a : ℝ ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]

Premises used: QuotientAddGroup.coe_mk', AddMonoidHom.map_zmultiples, AddSubgroup.map_comap_eq_self_of_surjective
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ Function.Surjective (α := ℝ) (β := AddCircle p)
    (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : ℝ) → AddCircle p)

Tactic:
Quot.mk_surjective

Premises used: Quotient, Quot.mk_surjective
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ Function.Surjective (α := ℝ) (β := AddCircle p)
    (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : ℝ) → AddCircle p)

Tactic:
exact Quot.mk_surjective

Premises used: Quot.mk_surjective
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ¬Dense (↑s : Set (AddCircle p))
mpr :
  ∀ (a : AddCircle p) (h : ¬Dense (↑(AddSubgroup.zmultiples a) : Set (AddCircle p))),
    ∃ (a_1 : AddCircle p),
      addOrderOf a_1 ≠ 0 ∧ Eq (α := AddSubgroup (AddCircle p)) (AddSubgroup.zmultiples a) (AddSubgroup.zmultiples a_1)
⊢ ∃ (a : AddCircle p), addOrderOf a ≠ 0 ∧ s = AddSubgroup.zmultiples a

Tactic:
obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a := by
      rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
        ← AddSubgroup.coe_comap, xor_iff_not_iff'.1 (AddSubgroup.dense_xor_cyclic _)] at h
      rcases h with ⟨a, ha⟩
      use a
      rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha,
        AddSubgroup.map_comap_eq_self_of_surjective]
      exact Quot.mk_surjective

Premises used: rfl
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
h : ¬Dense (↑(AddSubgroup.zmultiples a) : Set (AddCircle p))
⊢ ∃ (a_1 : AddCircle p),
    addOrderOf a_1 ≠ 0 ∧ Eq (α := AddSubgroup (AddCircle p)) (AddSubgroup.zmultiples a) (AddSubgroup.zmultiples a_1)

Tactic:
⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩

Premises used: AddCircle.denseRange_zsmul_iff, Iff.not, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
h : ¬Dense (↑(AddSubgroup.zmultiples a) : Set (AddCircle p))
⊢ ∃ (a_1 : AddCircle p),
    addOrderOf a_1 ≠ 0 ∧ Eq (α := AddSubgroup (AddCircle p)) (AddSubgroup.zmultiples a) (AddSubgroup.zmultiples a_1)

Tactic:
exact ⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
p : ℝ
⊢ PathConnectedSpace (AddCircle p)

Tactic:
inferInstanceAs <| PathConnectedSpace (Quotient _)

Premises used: _private.0.AddCircle.pathConnectedSpace._proof_1
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
p : ℝ
inst : Fact (0 < p)
rw : IsCompact (X := AddCircle p) (QuotientAddGroup.mk '' Icc 0 (0 + p))
⊢ CompactSpace (AddCircle p)

Tactic:
rw [← isCompact_univ_iff, ← coe_image_Icc_eq p 0]

Premises used: AddCircle.coe_image_Icc_eq, isCompact_univ_iff, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
p : ℝ
inst : Fact (0 < p)
⊢ IsCompact (X := AddCircle p) (QuotientAddGroup.mk '' Icc 0 (0 + p))

Tactic:
isCompact_Icc.image (AddCircle.continuous_mk' p)

Premises used: CompactIccSpace.isCompact_Icc, AddCircle.continuous_mk', IsCompact.image
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
p : ℝ
inst : Fact (0 < p)
⊢ IsCompact (X := AddCircle p) (QuotientAddGroup.mk '' Icc 0 (0 + p))

Tactic:
exact isCompact_Icc.image (AddCircle.continuous_mk' p)

Premises used: CompactIccSpace.isCompact_Icc, AddCircle.continuous_mk', IsCompact.image
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
p : ℝ
⊢ ProperlyDiscontinuousVAdd ↥(AddSubgroup.op (zmultiples p)) ℝ

Tactic:
(zmultiples p).properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite
    (AddSubgroup.tendsto_zmultiples_subtype_cofinite p)

Premises used: AddSubgroup.tendsto_zmultiples_subtype_cofinite, AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite, AddSubgroup.zmultiples
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
⊢ ∀ (a b : ℤ),
    (fun (j : ℤ) ↦
          ((↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) :
            HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)))
        (a + b) =
      HAdd.hAdd (α := UnitAddCircle)
        ((fun (j : ℤ) ↦
            ((↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) :
              HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)))
          a)
        ((fun (j : ℤ) ↦
            ((↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) :
              HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)))
          b)

Tactic:
simp [add_div]

Premises used: add_div
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
⊢ Eq (α := UnitAddCircle)
    ((AddMonoidHom.mk' (fun (j : ℤ) ↦ (↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)) ⋯ :
        (a : ℤ) → UnitAddCircle)
      (↑N : ℤ))
    0

Tactic:
simp [div_self (NeZero.ne _)]

Premises used: div_self, NeZero.ne
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
j : ℤ
⊢ Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) (↑j : ZMod N))
    (↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)

Tactic:
simp [toAddCircle]

Premises used: ZMod.toAddCircle
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
j : ℕ
⊢ Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) (↑j : ZMod N))
    (↑(HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)

Tactic:
simpa using toAddCircle_intCast (N := N) j

Premises used: Nat.cast, ZMod.toAddCircle_intCast
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
rw :
  Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle)
    ((toAddCircle : (a : ZMod N) → UnitAddCircle) (↑j.val : ZMod N) : UnitAddCircle)
rw₁ rw₂ :
  Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle)
    ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle)
⊢ Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle)
    ((↑(HDiv.hDiv (α := ℝ) (↑j.val : ℝ) (↑N : ℝ)) : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1)) :
      HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 1))

Tactic:
rw [← toAddCircle_natCast, natCast_zmod_val]

Premises used: ZMod.toAddCircle_natCast, ZMod.natCast_zmod_val
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) x : UnitAddCircle)
    ((toAddCircle : (a : ZMod N) → UnitAddCircle) y : UnitAddCircle)
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)

Tactic:
have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) x : UnitAddCircle)
    ((toAddCircle : (a : ZMod N) → UnitAddCircle) y : UnitAddCircle)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
hx :
  ∀
    (hxy :
      Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
        (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1))
    (this : LT.lt (α := ℝ) 0 (↑N : ℝ)), HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ) ∈ Ico 0 (HAdd.hAdd (α := ℝ) 0 1)
hy :
  ∀
    (hxy :
      Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
        (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1))
    (this : LT.lt (α := ℝ) 0 (↑N : ℝ)), HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ) ∈ Ico 0 (HAdd.hAdd (α := ℝ) 0 1)
rwa :
  (hxy :
      Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
        (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)) →
    (this : LT.lt (α := ℝ) 0 (↑N : ℝ)) → ℝ
⊢ x = y

Tactic:
rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico,
    div_left_inj' this.ne', Nat.cast_inj, (val_injective N).eq_iff] at hxy

Premises used: ZMod.val_injective, Function.Injective.eq_iff, AddCircle.coe_eq_coe_iff_of_mem_Ico, Nat.cast_inj, LT.lt.ne', ZMod.toAddCircle_apply, div_left_inj'
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ) < HAdd.hAdd (α := ℝ) 0 1

Tactic:
simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

Premises used: zero_add, div_lt_one, Nat.cast_lt, ZMod.val_lt
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ) ∈ Ico 0 (HAdd.hAdd (α := ℝ) 0 1)

Tactic:
exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ) < HAdd.hAdd (α := ℝ) 0 1

Tactic:
simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

Premises used: zero_add, div_lt_one, Nat.cast_lt, ZMod.val_lt
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
x y : ZMod N
hxy :
  Eq (α := UnitAddCircle) (↑(HDiv.hDiv (α := ℝ) (↑x.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
    (↑(HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ)) : ℝ ⧸ zmultiples 1)
this : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑y.val : ℝ) (↑N : ℝ) ∈ Ico 0 (HAdd.hAdd (α := ℝ) 0 1)

Tactic:
exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
j k : ZMod N
⊢ Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle)
      ((toAddCircle : (a : ZMod N) → UnitAddCircle) k : UnitAddCircle) ↔
    j = k

Tactic:
(toAddCircle_injective N).eq_iff

Premises used: Function.Injective.eq_iff, ZMod.toAddCircle_injective
-- Module: Mathlib.Topology.Instances.AddCircle.Real
Goal:
N : ℕ
inst : NeZero N
j : ZMod N
⊢ Eq (α := UnitAddCircle) ((toAddCircle : (a : ZMod N) → UnitAddCircle) j : UnitAddCircle) (0 : UnitAddCircle) ↔ j = 0

Tactic:
map_eq_zero_iff _ (toAddCircle_injective N)

Premises used: map_eq_zero_iff, ZMod.toAddCircle_injective
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ preCantorSet 0 = Set.Icc 0 1

Tactic:
rfl

Premises used: preCantorSet, rfl
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
⊢ preCantorSet (n + 1) = (fun (x : ℝ) ↦ x / 3) '' preCantorSet n ∪ (fun (x : ℝ) ↦ (2 + x) / 3) '' preCantorSet n

Tactic:
rfl

Premises used: preCantorSet, rfl
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (1 / 4) ∧ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (3 / 4)

Tactic:
⟨⟨ ?_, ?_⟩, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
zero : 0 ≤ 1 / 4
zero₁ : 1 / 4 ≤ 1
zero₂ : 0 ≤ 3 / 4
zero₃ : 3 / 4 ≤ 1
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (1 / 4) ∧ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (3 / 4)

Tactic:
refine ⟨⟨ ?_, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 0 ≤ 1 / 4

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 1 / 4 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 0 ≤ 3 / 4

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 3 / 4 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
succ : 1 / 4 ∈ preCantorSet (n + 1)
succ₁ : 3 / 4 ∈ preCantorSet (n + 1)
⊢ 1 / 4 ∈ preCantorSet (n + 1) ∧ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
apply And.intro

Premises used: And.intro
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun (x : ℝ) ↦ x / 3) (3 / 4) = 1 / 4

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun (x : ℝ) ↦ (2 + x) / 3) (1 / 4) = 3 / 4

Tactic:
norm_num
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
zero : 1 / 4 ∈ preCantorSet 0 ∧ 3 / 4 ∈ preCantorSet 0
succ :
  ∀ (n : ℕ) (ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n),
    1 / 4 ∈ preCantorSet (n + 1) ∧ 3 / 4 ∈ preCantorSet (n + 1)
⊢ 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n

Tactic:
induction n with
  | zero =>
    simp only [preCantorSet_zero]
    refine ⟨⟨ ?_, ?_⟩, ?_, ?_⟩ <;> norm_num
  | succ n ih =>
    apply And.intro
    · -- goal: 1 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 3 / 4 ∈ preCantorSet n
      exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩
    · -- goal: 3 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 1 / 4 ∈ preCantorSet n
      exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

Premises used: preCantorSet_zero, And.intro, Or.inl, Or.inr
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
⊢ 1 / 4 ∈ preCantorSet n

Tactic:
(quarters_mem_preCantorSet n).1

Premises used: quarters_mem_preCantorSet, And.left
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 1 / 4 ∈ cantorSet

Tactic:
Set.mem_iInter.mpr quarter_mem_preCantorSet

Premises used: Iff.mpr, Set.Mem, Set.mem_iInter, cantorSet, quarter_mem_preCantorSet
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 0 ∈ preCantorSet 0

Tactic:
simp [preCantorSet]

Premises used: preCantorSet
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 0 ∈ preCantorSet n
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ x / 3) 0) 0

Tactic:
simp only [zero_div]

Premises used: zero_div
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
ih : 0 ∈ preCantorSet n
⊢ 0 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
zero : 0 ∈ preCantorSet 0
succ : ∀ (n : ℕ) (ih : 0 ∈ preCantorSet n), 0 ∈ preCantorSet (n + 1)
⊢ 0 ∈ preCantorSet n

Tactic:
induction n with
  | zero =>
    simp [preCantorSet]
  | succ n ih =>
    exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

Premises used: preCantorSet, Or.inl
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ 0 ∈ cantorSet

Tactic:
simp [cantorSet, zero_mem_preCantorSet]

Premises used: zero_mem_preCantorSet, cantorSet
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ Antitone preCantorSet

Tactic:
antitone_nat_of_succ_le fun m ↦ ?_

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
refine : ∀ (m : ℕ), preCantorSet (m + 1) ≤ preCantorSet m
⊢ Antitone preCantorSet

Tactic:
refine antitone_nat_of_succ_le fun m ↦ ?_

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ preCantorSet (HAdd.hAdd (α := ℕ) 0 1) ⊆ preCantorSet 0

Tactic:
grind [preCantorSet_zero, preCantorSet_succ]

Premises used: preCantorSet_succ, preCantorSet_zero
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
h : preCantorSet (n + 1) ⊆ preCantorSet n
⊢ preCantorSet (n + 1 + 1) ⊆ preCantorSet (n + 1)

Tactic:
grind [preCantorSet_zero, preCantorSet_succ]

Premises used: preCantorSet_succ, preCantorSet_zero
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
m : ℕ
zero : preCantorSet (HAdd.hAdd (α := ℕ) 0 1) ⊆ preCantorSet 0
succ : ∀ (n : ℕ), preCantorSet (n + 1) ⊆ preCantorSet n → preCantorSet (n + 1 + 1) ⊆ preCantorSet (n + 1)
⊢ preCantorSet (m + 1) ⊆ preCantorSet m

Tactic:
induction m with grind [preCantorSet_zero, preCantorSet_succ]

Premises used: preCantorSet_succ, preCantorSet_zero
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
⊢ 0 ≤ n

Tactic:
simp
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
n : ℕ
⊢ preCantorSet n ⊆ preCantorSet 0

Tactic:
exact preCantorSet_antitone (by simp)

Premises used: preCantorSet_antitone
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ cantorSet ⊆ Set.Icc 0 1

Tactic:
Set.iInter_subset _ 0

Premises used: cantorSet, preCantorSet, Set.iInter_subset, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
rw :
  Eq (α := Set ℝ) (⋂ (n : ℕ), preCantorSet n)
    ((⋂ (i : ℕ), (fun (x : ℝ) ↦ x / 3) '' preCantorSet i) ∪ ⋂ (i : ℕ), (fun (x : ℝ) ↦ (2 + x) / 3) '' preCantorSet i)
hf : Function.Bijective (β := ℝ) fun (x : ℝ) ↦ (2 + x) / 3
hf₁ : Function.Bijective (β := ℝ) fun (x : ℝ) ↦ x / 3
⊢ Eq (α := Set ℝ) (⋂ (n : ℕ), preCantorSet n)
    (((fun (x : ℝ) ↦ x / 3) '' ⋂ (n : ℕ), preCantorSet n) ∪ (fun (x : ℝ) ↦ (2 + x) / 3) '' ⋂ (n : ℕ), preCantorSet n)

Tactic:
rw [Set.image_iInter, Set.image_iInter]

Premises used: Set.image_iInter
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ Ne (α := ℝ) 3⁻¹ 0

Tactic:
simp