-- 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 :
  ((HPow.hPow (α := ℝ) 3 n1)⁻¹ * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((HPow.hPow (α := ℝ) 3 n1)⁻¹ * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ +
      2 * (3⁻¹ * (HPow.hPow (α := ℝ) 3 n1)⁻¹)
linarith :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₁ linarith₂ linarith₃ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₄ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₅ linarith₆ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₇ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₈ linarith₉ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₀ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    GT.gt (α := ℝ) 3 0
linarith₁₁ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₂ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₁₃ linarith₁₄ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₅ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₆ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₁₇ linarith₁₈ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₁₉ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    3 / 3 = 1
linarith₂₀ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₂₁ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 3 1 = 3
linarith₂₂ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    HMul.hMul (α := ℝ) 1 3 = 3
linarith₂₃ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    GT.gt (α := ℝ) 3 0
linarith₂₄ :
  (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) <
      (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
        ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) →
    -(1 * (HPow.hPow (α := ℝ) 3 n1)⁻¹ * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 -
            (1 * (HPow.hPow (α := ℝ) 3 n1)⁻¹ * (1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) *
                HMul.hMul (α := ℝ) 1 1 +
              HMul.hMul (α := ℝ) 1 2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (HPow.hPow (α := ℝ) 3 n1)⁻¹)))) +
        (1 * (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
            ((1 * ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1) -
          1 * (HPow.hPow (α := ℝ) 3 n1)⁻¹ *
            ((1 * ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * HMul.hMul (α := ℝ) 1 1 + HMul.hMul (α := ℝ) 1 2)) =
      0
⊢ (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) =
    (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹)
have linarith₂₅ : (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ b (1 + n1 + i)) * 3⁻¹ + HMul.hMul (α := ℝ) 2 3⁻¹) <
    (HPow.hPow (α := ℝ) 3 n1)⁻¹ * ((ofDigits (b := 3) fun (i : ℕ) ↦ a (1 + n1 + i)) * 3⁻¹) →
  3 / 3 = 1
Tactic: linarith