-- Lean 4 proof step from Mathlib.Topology.Instances.CantorSet (goal)
Goal:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ (n : ℕ) (hn : n < n1), a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : Eq (α := ℝ) (∑ x ∈ Finset.range n1, ofDigitsTerm a x) (∑ x ∈ Finset.range n1, ofDigitsTerm b x)
h :
  ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 +
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x +
        (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) +
      ofDigitsTerm b n1
linarith :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    3 / 3 = 1
linarith₂ linarith₃ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₄ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    3 / 3 = 1
linarith₆ linarith₇ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₈ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    GT.gt (α := ℝ) 3 0
linarith₉ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₀ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    3 / 3 = 1
linarith₁₁ linarith₁₂ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₃ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₄ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    3 / 3 = 1
linarith₁₅ linarith₁₆ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₇ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    GT.gt (α := ℝ) 3 0
linarith₁₈ :
  ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) <
      (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 →
    -(HMul.hMul (α := ℝ) 3 (∑ x ∈ Finset.range n1, ofDigitsTerm b x) + 3 * ofDigitsTerm a n1 +
              1 * (1 / 3) ^ n1 * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 -
            (HMul.hMul (α := ℝ) 3 (∑ x ∈ Finset.range n1, ofDigitsTerm b x) +
                1 * (1 / 3) ^ n1 * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 +
              3 * ofDigitsTerm b n1)) +
        (3 * ofDigitsTerm a n1 +
            1 * (1 / 3) ^ n1 * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 -
          (1 * (1 / 3) ^ n1 * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 +
            3 * ofDigitsTerm b n1)) =
      0
linarith₁₉ :
  (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 <
      ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) →
    HMul.hMul (α := ℝ) 1 1 = 1
⊢ ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) =
    (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1
have linarith₂₀ : (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 <
    ofDigitsTerm a n1 + (HPow.hPow (α := ℝ) 3⁻¹ n1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * (1 / 3) →
  3 / 3 = 1
Tactic: linarith