-- 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
⊢ (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 : ℕ) ↦ 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
Tactic: linarith