awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
⊢ -r < -1
have linarith : -1 ≤ -r → -1 + (2 - r) + (-1 - -r) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
have h : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) {x : ℝ | Liouville x} x ↔
    Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ),
            ⋃ (_ : 1 < b),
              ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
                {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ IsGδ (X := ℝ) {x : ℝ | Liouville x}
have rw : IsGδ (X := ℝ)
  (⋂ (n : ℕ),
    ⋃ (a : ℤ),
      ⋃ (b : ℤ),
        ⋃ (_ : 1 < b),
          ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
            {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
Tactic: rw [setOf_liouville_eq_iInter_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ IsGδ (X := ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
have refine : ∀ (n : ℕ),
  IsOpen (X := ℝ)
    (⋃ (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δ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
n : ℕ
⊢ IsOpen (X := ℝ)
    (⋃ (a : ℤ),
      ⋃ (b : ℤ),
        ⋃ (_ : 1 < b),
          ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
            {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
have refine : ∀ (a b : ℤ) (_hb : 1 < b),
  IsOpen
    (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 => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
have 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))
Tactic: refine Subset.antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
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))
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
have 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}
Tactic: refine Subset.antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Subset (α := Set ℝ) {x : ℝ | Liouville x}
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
have refine_1 : Subset (α := Set ℝ) {x : ℝ | Liouville 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) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Subset (α := Set ℝ) {x : ℝ | Liouville x}
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
have 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))
Tactic: rw [setOf_liouville_eq_iInter_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Subset (α := Set ℝ)
    ({x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
    {x : ℝ | Liouville x}
have 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 : ℝ)})
Tactic: simp only [inter_iInter, inter_iUnion, setOf_liouville_eq_iInter_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
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 : ℝ)})
have 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 : ℝ)}
Tactic: refine iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
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 : ℝ)}
have 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 : ℝ)}
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
n : ℕ
a b : ℤ
hb : 1 < b
⊢ (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : ℝ) = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
have norm_cast : Rat.divInt a b = Rat.divInt a b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x
have rw : {x : ℝ | Irrational x} ∩
    ⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∈
  residual ℝ
Tactic: rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ {x : ℝ | Irrational x} ∩
      ⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) ∈
    residual ℝ
have refine : Filter.Eventually
  (Membership.mem (γ := Set ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
  (residual ℝ)
Tactic: refine eventually_residual_irrational.and ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
⊢ Filter.Eventually
    (Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
    (residual ℝ)
have refine_1 : IsGδ (X := ℝ)
  {x : ℝ |
    Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n))
      x}
Tactic: refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
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}
⊢ Filter.Eventually
    (Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ), ⋃ (_ : 1 < b), ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n)))
    (residual ℝ)
have 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}
Tactic: refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
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 : ℝ)
have 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 : ℝ)
Tactic: simp only [mem_iInter, mem_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
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 : ℝ)
have refine_2 : ∀ (n : ℕ), 1 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2
Tactic: refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
refine_2 : ∀ (n : ℕ), 1 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 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 : ℝ)
have refine_2₁ : ∀ (n : ℕ),
  (↑r : ℝ) ∈
    ball (HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ))
      (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n)
Tactic: refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (hypothesis)
Goal:
r : ℚ
n : ℕ
⊢ 1 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2
have this : 0 < r.den
Tactic: have := r.pos
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
n : ℕ
⊢ (↑r : ℝ) ∈
    ball (HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ))
      (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n)
have h : HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) = (↑r : ℝ)
Tactic: convert! @mem_ball_self ℝ _ (r : ℝ) _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
n : ℕ
h : HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) = (↑r : ℝ)
⊢ (↑r : ℝ) ∈
    ball (HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ))
      (1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n)
have refine_2 : 0 < 1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n
Tactic: convert! @mem_ball_self ℝ _ (r : ℝ) _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(r.num * 2) : ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) = (↑r : ℝ)
have h : HMul.hMul (α := ℝ) (↑r.num : ℝ) 2 / HMul.hMul (α := ℝ) (↑r.den : ℝ) 2 = (↑r : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
n : ℕ
⊢ HMul.hMul (α := ℝ) (↑r.num : ℝ) 2 / HMul.hMul (α := ℝ) (↑r.den : ℝ) 2 = (↑r : ℝ)
have h : Rat.divInt (r.num * 2) (↑(r.den * 2) : ℤ) = r
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Residual (goal)
Goal:
r : ℚ
n : ℕ
⊢ 0 < 1 / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℤ) (↑r.den : ℤ) 2) : ℝ) n
have refine_2 : 0 < HMul.hMul (α := ℤ) (↑r.den : ℤ) 2
Tactic: refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (hypothesis)
Goal:
x : ↥(divisorsAntidiagonal 1)
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)
have h : (↑x : ℕ × ℕ).1 * (↑x : ℕ × ℕ).2 = 1 ∧ Ne (α := ℕ) 1 0
Tactic: have h := Nat.mem_divisorsAntidiagonal.mp x.2
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (hypothesis)
Goal:
x : ↥(divisorsAntidiagonal 1)
h : (↑x : ℕ × ℕ).1 * (↑x : ℕ × ℕ).2 = 1 ∧ Ne (α := ℕ) 1 0
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)
have h₁ : (↑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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (hypothesis)
Goal:
n : ℕ+
k l : ℕ
h : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
⊢ Eq (α := (n : ℕ+) × ↥(↑n : ℕ).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))))
    (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
      (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h))
have h₁ : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
Tactic: rw [Nat.mem_divisorsAntidiagonal] at h
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
n : ℕ+
k l : ℕ
h_1 : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
⊢ Eq (α := (n : ℕ+) × ↥(↑n : ℕ).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.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
      (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))
have a : 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 : ℕ)) sorry)
            (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
              x_1 ∈ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) sorry) : ℕ).divisorsAntidiagonal)
              ((↑x.1 : ℕ), (↑x.2 : ℕ)) sorry) :
          (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: ext
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n / (1 - r ^ n)
have simp : Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n * (1 / (1 - r ^ n))
Tactic: simp only [div_eq_mul_one_div (_ * _ ^ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n * (1 / (1 - r ^ n))
have apply : Tendsto (fun (n : ℕ) ↦ 1 / (1 - r ^ n)) cofinite (𝓝 (1 / HSub.hSub (α := 𝕜) 1 0))
Tactic: apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
    (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable.{u_1, 0} (α := 𝕜) fun (c : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
    HPow.hPow (α := 𝕜) (↑(↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
      r ^
        ((↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
          (↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)
have hf : Summable (α := ℝ) fun (a : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
  ‖HPow.hPow (α := 𝕜) (↑(↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
      r ^
        ((↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
          (↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)‖
Tactic: apply Summable.of_norm
-- Lean 4 proof step from Mathlib.NumberTheory.TsumDivisorsAntidiagonal (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (a : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
    ‖HPow.hPow (α := 𝕜) (↑(↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
        r ^
          ((↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
            (↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)‖
have hf : (∀ (x : ℕ+),
    Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖) ∧
  Summable (α := ℝ) fun (x : ℕ+) ↦
    ∑' (y : ↥(↑x : ℕ).divisorsAntidiagonal),
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖
Tactic: rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]