awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine :
  ∀ (n : ℕ),
    IsOpen (X := ℝ)
      (⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
⊢ IsGδ (X := ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
refine .iInter fun n => IsOpen.isGδ ?_
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
⊢ IsOpen (X := ℝ)
    (⋃ (a : ℤ),
      ⋃ (b : ℤ),
        ⋃ (_ : 1 < b),
          ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
            {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_

Premises used: isOpen_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
refine :
  ∀ (a b : ℤ) (_hb : 1 < b),
    IsOpen
      (ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
        {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
⊢ IsOpen (X := ℝ)
    (⋃ (a : ℤ),
      ⋃ (b : ℤ),
        ⋃ (_ : 1 < b),
          ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
            {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_

Premises used: isOpen_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen
    (ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
      {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
isOpen_ball.inter isClosed_singleton.isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, Set.diff, setOf, Metric.isOpen_ball, IsOpen.inter, Not
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen
    (ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
      {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
exact isOpen_ball.inter isClosed_singleton.isOpen_compl

Premises used: IsClosed.isOpen_compl, Metric.isOpen_ball, IsOpen.inter
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_1 :
  Subset (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
refine_2 :
  Subset (α := Set ℝ)
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
    {x : ℝ | Liouville x}
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
refine Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Subset (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
subset_inter (fun x hx => hx.irrational) ?_

Premises used: Liouville.irrational, Set.subset_inter
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_1 :
  Subset (α := Set ℝ) {x : ℝ | Liouville x}
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
⊢ Subset (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
refine subset_inter (fun x hx => hx.irrational) ?_

Premises used: Set.subset_inter
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_1 :
  Subset (α := Set ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
⊢ Subset (α := Set ℝ) {x : ℝ | Liouville x}
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
rw [setOf_liouville_eq_iInter_iUnion]

Premises used: setOf_liouville_eq_iInter_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Subset (α := Set ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => diff_subset

Premises used: Set.diff_subset, Set.iUnion₂_mono, Set.iUnion_mono, Set.iInter_mono
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Subset (α := Set ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))

Tactic:
exact iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => diff_subset

Premises used: Set.diff_subset, Set.iUnion₂_mono, Set.iUnion_mono, Set.iInter_mono
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_2 :
  Subset (α := Set ℝ)
    (⋂ (i : ℕ),
      ⋃ (i_1 : ℤ),
        ⋃ (i_2 : ℤ),
          ⋃ (_ : 1 < i_2),
            {x : ℝ | Irrational x} ∩
              ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i))
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
⊢ Subset (α := Set ℝ)
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
    {x : ℝ | Liouville x}

Tactic:
simp only [inter_iInter, inter_iUnion, setOf_liouville_eq_iInter_iUnion]

Premises used: Set.inter_iInter, Set.inter_iUnion, setOf_liouville_eq_iInter_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Subset (α := Set ℝ)
    (⋂ (i : ℕ),
      ⋃ (i_1 : ℤ),
        ⋃ (i_2 : ℤ),
          ⋃ (_ : 1 < i_2),
            {x : ℝ | Irrational x} ∩
              ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i))
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_

Premises used: Set.iUnion₂_mono, Set.iUnion_mono, Set.iInter_mono
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_2 :
  ∀ (n : ℕ) (a b : ℤ) (hb : 1 < b),
    {x : ℝ | Irrational x} ∩ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ⊆
      ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
        {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)}
⊢ Subset (α := Set ℝ)
    (⋂ (i : ℕ),
      ⋃ (i_1 : ℤ),
        ⋃ (i_2 : ℤ),
          ⋃ (_ : 1 < i_2),
            {x : ℝ | Irrational x} ∩
              ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i))
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
refine iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_

Premises used: Set.iUnion₂_mono, Set.iUnion_mono, Set.iInter_mono
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
a b : ℤ
hb : 1 < b
refine_2 :
  ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∩ {x : ℝ | Irrational x} ⊆
    ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
      {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)}
⊢ {x : ℝ | Irrational x} ∩ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ⊆
    ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
      {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)}

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
a b : ℤ
hb : 1 < b
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Rat.divInt a b = Rat.divInt a b
⊢ (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : ℝ) = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∩ {x : ℝ | Irrational x} ⊆
    ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
      {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)}

Tactic:
exact diff_subset_diff Subset.rfl (singleton_subset_iff.2 ⟨a / b, by norm_cast⟩)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
rw :
  {x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∈
    residual ℝ
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x

Tactic:
rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]

Premises used: Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ {x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∈
    residual ℝ

Tactic:
eventually_residual_irrational.and ?_

Premises used: eventually_residual_irrational, Set.Mem, Filter.Eventually, setOf, Filter.Eventually.and, Set.inter, Irrational, Not
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine :
  Filter.Eventually
    (Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
    (residual ℝ)
⊢ {x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∈
    residual ℝ

Tactic:
refine eventually_residual_irrational.and ?_

Premises used: eventually_residual_irrational, Filter.Eventually.and
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Filter.Eventually
    (Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
    (residual ℝ)

Tactic:
residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)

Premises used: IsDenseEmbedding.toIsDenseInducing, Rat.isDenseEmbedding_coe_real, Filter.Eventually, Dense.mono, IsDenseInducing.dense, residual_of_dense_Gδ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
refine_1 :
  IsGδ (X := ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
        x}
refine_2 :
  Subset (α := Set ℝ) (range Rat.cast)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
        x}
⊢ Filter.Eventually
    (Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
    (residual ℝ)

Tactic:
refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)

Premises used: IsDenseEmbedding.toIsDenseInducing, Rat.isDenseEmbedding_coe_real, Dense.mono, IsDenseInducing.dense, residual_of_dense_Gδ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ IsGδ (X := ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
        x}

Tactic:
.iInter fun n => IsOpen.isGδ <|
          isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball

Premises used: iInf, Set.Mem, Set.iInter, setOf, IsGδ.iInter, Metric.isOpen_ball, isOpen_iUnion, IsOpen.isGδ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ IsGδ (X := ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
        x}

Tactic:
exact .iInter fun n => IsOpen.isGδ <|
          isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
refine_2 :
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∀ (i : ℕ),
        ∃ (i_1 : ℤ) (i_2 : ℤ) (_ : 1 < i_2),
          x ∈ ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i)}
    (↑r : ℝ)
⊢ Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
        x}
    (↑r : ℝ)

Tactic:
simp only [mem_iInter, mem_iUnion]

Premises used: Set.mem_iUnion, Set.mem_iInter
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
⊢ Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∀ (i : ℕ),
        ∃ (i_1 : ℤ) (i_2 : ℤ) (_ : 1 < i_2),
          x ∈ ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i)}
    (↑r : ℝ)

Tactic:
fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩

Premises used: Rat.num, HMul.hMul, Set.Mem, setOf, Rat.den, Nat.cast, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
refine_2 : ∀ (n : ℕ), 1 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2
refine_2₁ :
  ∀ (n : ℕ),
    (↑r : ℝ) ∈
      ball (HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ))
        (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n)
⊢ Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∀ (i : ℕ),
        ∃ (i_1 : ℤ) (i_2 : ℤ) (_ : 1 < i_2),
          x ∈ ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i_2 : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i_2 : ℝ) i)}
    (↑r : ℝ)

Tactic:
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ 0 < r.den

Tactic:
have := r.pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
this : 0 < r.den
⊢ 1 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (ball (↑r : ℝ) (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n))
    (↑r : ℝ)

Tactic:
@mem_ball_self ℝ _ (r : ℝ) _ _

Premises used: Metric.mem_ball_self
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
h : HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) = (↑r : ℝ)
refine_2 : 0 < 1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n
⊢ (↑r : ℝ) ∈
    ball (HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ))
      (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n)

Tactic:
convert! @mem_ball_self ℝ _ (r : ℝ) _ _

Premises used: Metric.mem_ball_self
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
h : HMul.hMul (α := ℝ) (↑r.num : ℝ) 2 / HMul.hMul (α := ℝ) (↑r.den : ℝ) 2 = (↑r : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) = (↑r : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
h : Rat.divInt (r.num * 2) (↑(r.den * 2) : ℤ) = r
⊢ HMul.hMul (α := ℝ) (↑r.num : ℝ) 2 / HMul.hMul (α := ℝ) (↑r.den : ℝ) 2 = (↑r : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) (↑(r.den * 2) : ℤ) = r

Tactic:
simp [Rat.divInt_mul_right (two_ne_zero)]

Premises used: two_ne_zero, Rat.divInt_mul_right
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ 0 < 1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n

Tactic:
one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)

Premises used: Iff.mpr, pow_pos, one_div_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
refine_2 : 0 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2
⊢ 0 < 1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n

Tactic:
refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)

Premises used: Iff.mpr, pow_pos, one_div_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ 0 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2

Tactic:
mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two

Premises used: Iff.mpr, Rat.pos, mul_pos, zero_lt_two, Int.natCast_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
r : ℚ
n : ℕ
⊢ 0 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2

Tactic:
exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two

Premises used: Iff.mpr, Rat.pos, mul_pos, zero_lt_two, Int.natCast_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ Dense (X := ℝ) {x : ℝ | Liouville x}

Tactic:
dense_of_mem_residual eventually_residual_liouville

Premises used: dense_of_mem_residual, eventually_residual_liouville
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
n : ℕ+
x : ↥(↑n : ℕ).divisorsAntidiagonal
⊢ (↑(divisorsAntidiagonalFactors n x).1 : ℕ) * (↑(divisorsAntidiagonalFactors n x).2 : ℕ) = (↑n : ℕ)

Tactic:
simp [divisorsAntidiagonalFactors, (Nat.mem_divisorsAntidiagonal.mp x.2).1]

Premises used: divisorsAntidiagonalFactors, Nat.mem_divisorsAntidiagonal, And.left, Iff.mp, Subtype.property
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ↥(divisorsAntidiagonal 1)
⊢ (↑x : ℕ × ℕ).1 * (↑x : ℕ × ℕ).2 = 1 ∧ Ne (α := ℕ) 1 0

Tactic:
have h := Nat.mem_divisorsAntidiagonal.mp x.2
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ↥(divisorsAntidiagonal 1)
h : (↑x : ℕ × ℕ).1 * (↑x : ℕ × ℕ).2 = 1 ∧ Ne (α := ℕ) 1 0
⊢ (↑x : ℕ × ℕ).1 = 1 ∧ (↑x : ℕ × ℕ).2 = 1

Tactic:
simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h

Premises used: and_true, ne_eq, mul_eq_one, one_ne_zero, not_false_eq_true
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ↥(divisorsAntidiagonal 1)
h : (↑x : ℕ × ℕ).1 = 1 ∧ (↑x : ℕ × ℕ).2 = 1
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)

Tactic:
simp [divisorsAntidiagonalFactors, h.1, h.2]

Premises used: divisorsAntidiagonalFactors, And.right, And.left
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ℕ+ × ℕ+
⊢ ((↑x.1 : ℕ), (↑x.2 : ℕ)) ∈
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) : ℕ).divisorsAntidiagonal

Tactic:
simp [Nat.mem_divisorsAntidiagonal]

Premises used: Nat.mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
n : ℕ+
k l : ℕ
h : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
⊢ (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0

Tactic:
rw [Nat.mem_divisorsAntidiagonal] at h

Premises used: Nat.mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
n : ℕ+
k l : ℕ
h_1 : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
⊢ Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
      ((fun (x : ℕ+ × ℕ+) ↦
          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
              (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
              (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                x_1 ∈ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) : ℕ).divisorsAntidiagonal)
                ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
            (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
        ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
            divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
              (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) =
    Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
      (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
        (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))

Tactic:
simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]

Premises used: divisorsAntidiagonalFactors, PNat.coe_injective, Function.Injective.eq_iff, And.left