-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
hI₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
inr :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      (HSMul.hSMul (β := ℝ≥0∞) (addOrderOf (u j))
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
            (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
          ℝ≥0∞))
inr₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(addOrderOf (u j)) : ℝ≥0∞) : ℝ≥0∞)
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
            (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
          ℝ≥0∞))
inr₃ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
        ((↑(addOrderOf (u j)) : ℝ≥0∞) : ℝ≥0∞))
      ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
          (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
        ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr₄ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞))
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))) : ℝ≥0∞)
Tactic: rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]