-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : PseudoMetricSpace X
inst_5 : MeasurableSpace X
inst_6 : PseudoMetricSpace Y
inst_7 : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst_8 : SFinite ν
inst_9 : IsUnifLocDoublingMeasure μ
inst_10 : IsUnifLocDoublingMeasure ν
r : ℝ
hμr :
  ∀ (x : X),
    (μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
hνr :
  ∀ (x : Y),
    (ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
x : X × Y
h :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞))
      ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 (2 * r)) : ℝ≥0∞) ≤
    (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
        ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
h₁ :
  HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞) ≤
    (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
        ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
h₂ :
  HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞) ≤
    (↑(doublingConstant μ) : ℝ≥0∞) * (↑(doublingConstant ν) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
        ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 (2 * r)) : ℝ≥0∞)
      ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 (2 * r)) : ℝ≥0∞) ≤
    (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
        ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
have h₃ : (↑(doublingConstant μ) : ℝ≥0∞) * (↑(doublingConstant ν) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
      ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞) ≤
  (↑(doublingConstant μ) : ℝ≥0∞) * (↑(doublingConstant ν) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
      ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
Tactic: grw [hμr, hνr, ENNReal.coe_mul, mul_mul_mul_comm]