-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
inr :
  HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
      HMul.hMul (α := ℝ) (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c)
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
inr₁ :
  HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c) *
      HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
inr₂ :
  1 *
      HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
⊢ HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
      ∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        HMul.hMul (α := ℝ) (β := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) c : ℝ)
          (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i) : ℝ) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
have inr₃ : HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
    (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
  HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
Tactic: rw [finprod_mul_distrib (by fun_prop) (by fun_prop),
    mul_mul_mul_comm, product_formula hc, one_mul]