How to handle 'Multipliable' statements produced by tprod

Stream: general

[Zhu]

Hi.
I'm currently working on proving something with an infinite product in Lean4 like this:

import Mathlib


example (a : ℝ) (ha : 0 < a ∧ a < 1) :
    ∏' n, (1 - a ^ (2 ^ (n + 1))) / (1 - a ^ (2 ^ n)) = 1 / (1 - a ^ (2 ^ 0)) := by
  simp only [div_eq_mul_inv]
  rw [tprod_mul, mul_comm]
  rw [tprod_eq_zero_mul']
  rw [mul_assoc, ← tprod_mul]
  have : ∀ b, (1 - a ^ 2 ^ (b + 1))⁻¹ * (1 - a ^ 2 ^ (b + 1)) = 1 := by
    intro b
    rw [inv_mul_cancel₀]
    apply sub_ne_zero_of_ne
    symm
    -- this part is annoying too, but I think I can fix it..
    sorry
  . simp [this]

  -- I'm comfused about the rest of these 'Multipliable' statements.
  . show Multipliable fun b => (1 - a ^ 2 ^ (b + 1))⁻¹
    sorry
  . show Multipliable fun b => 1 - a ^ 2 ^ (b + 1)
    sorry
  . sorry
  . sorry
  . sorry

Specifically, I'm stuck on the part where I need to handle the 'Multipliable' statements. I'm not sure how to proceed with those. Any insights or advice would be helpful.

[Eric Wieser]

I would recommend starting your proof with apply HasProd.tprod_eq so that the Multipliable goals never appear

[Zhu]

Thanks, I'll give that a try.