Level set family from base

theorem level_set_family_from_base    {B : Set E} {E_lam : ℝ → Set E} {A θ : ℝ}    (hB_meas : MeasurableSet B) (hB_fin : volume B ≠ ⊤)    (hE_sub : ∀ lam, E_lam lam ⊆ B)    (hE_meas : ∀ lam, MeasurableSet (E_lam lam))    (hE_anti : ∀ lam₁ lam₂, lam₁ ≤ lam₂ → E_lam lam₂ ⊆ E_lam lam₁)    (hA : 0 < A) (hθ_pos : 0 < θ) (hθ_lt : θ < 1)    (h_decay : ∀ lam : ℝ, A ≤ lam →      volume (E_lam (lam + A)) ≤ ENNReal.ofReal θ * volume (E_lam lam))    (t : ℝ) (_ht : 0 < t) :    volume (E_lam t) ≤      ENNReal.ofReal (1 / θ ^ 2) * volume B *        ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by  have h_decayF : ∀ s : ℝ, 0 < s →      volume (E_lam (s + A + A)) ≤ ENNReal.ofReal θ * volume (E_lam (s + A)) := by    intro s hs    have hsA : A ≤ s + A := by linarith    simpa [add_assoc] using h_decay (s + A) hsA  set F : ℝ → Set E := fun s => E_lam (s + A) with hF_def  have hF_sub : ∀ s, F s ⊆ B := by    intro s    simpa [F] using hE_sub (s + A)  have hF_meas : ∀ s, MeasurableSet (F s) := by    intro s    simpa [F] using hE_meas (s + A)  have hF_anti : ∀ s₁ s₂, s₁ ≤ s₂ → F s₂ ⊆ F s₁ := by    intro s₁ s₂ hs    simpa [F] using hE_anti (s₁ + A) (s₂ + A) (by linarith)  have h_iter :=    john_nirenberg_iteration hB_meas hB_fin hF_sub hF_meas hF_anti hA hθ_pos hθ_lt      (by        intro s hs        simpa [F, add_assoc] using h_decayF s hs)  have hAdiv : A * (-Real.log θ / A) = -Real.log θ := by    field_simp [hA.ne']  have hexpA : Real.exp (-A * (-Real.log θ / A)) = θ := by    have hexp_arg : -A * (-Real.log θ / A) = Real.log θ := by      calc        -A * (-Real.log θ / A) = -(A * (-Real.log θ / A)) := by ring        _ = -(-Real.log θ) := by rw [hAdiv]        _ = Real.log θ := by ring    rw [hexp_arg, Real.exp_log hθ_pos]  by_cases htA : A < t  · have hs_pos : 0 < t - A := by linarith    have hmain :        volume (E_lam t) ≤          ENNReal.ofReal (1 / θ) * volume B *            ENNReal.ofReal (Real.exp (-(t - A) * (-Real.log θ / A))) := by      simpa [F, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using        h_iter (t - A) hs_pos    have hexp_shift :        Real.exp (-(t - A) * (-Real.log θ / A)) =          (1 / θ) * Real.exp (-t * (-Real.log θ / A)) := by      have h_inv : (1 / θ : ℝ) = Real.exp (-Real.log θ) := by        rw [Real.exp_neg, Real.exp_log hθ_pos, one_div]      rw [h_inv, ← Real.exp_add]      congr 1      calc        -(t - A) * (-Real.log θ / A)            = -t * (-Real.log θ / A) + A * (-Real.log θ / A) := by ring        _ = -t * (-Real.log θ / A) + (-Real.log θ) := by rw [hAdiv]        _ = -Real.log θ + -t * (-Real.log θ / A) := by ring    calc      volume (E_lam t)          ≤ ENNReal.ofReal (1 / θ) * volume B *              ENNReal.ofReal (Real.exp (-(t - A) * (-Real.log θ / A))) := hmain      _ = ENNReal.ofReal (1 / θ ^ 2) * volume B *            ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by        rw [hexp_shift, ENNReal.ofReal_mul (by positivity)]        calc          ENNReal.ofReal (1 / θ) * volume B *              (ENNReal.ofReal (1 / θ) * ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))))              =              (ENNReal.ofReal (1 / θ) * ENNReal.ofReal (1 / θ)) * volume B *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                ring          _ = ENNReal.ofReal ((1 / θ) * (1 / θ)) * volume B *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                rw [← ENNReal.ofReal_mul (by positivity)]          _ = ENNReal.ofReal (1 / θ ^ 2) * volume B *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                congr 1                field_simp [pow_two, hθ_pos.ne']  · have ht_le_A : t ≤ A := le_of_not_gt htA    have hsub : E_lam t ⊆ B := hE_sub t    have hrate_pos : 0 < -Real.log θ / A := by      have hlog_neg : Real.log θ < 0 := Real.log_neg hθ_pos hθ_lt      exact div_pos (by linarith) hA    have hexp_lower : θ ≤ Real.exp (-t * (-Real.log θ / A)) := by      have hArg : -A * (-Real.log θ / A) ≤ -t * (-Real.log θ / A) := by        nlinarith [ht_le_A, le_of_lt hrate_pos]      calc        θ = Real.exp (-A * (-Real.log θ / A)) := by rw [hexpA]        _ ≤ Real.exp (-t * (-Real.log θ / A)) := Real.exp_le_exp.2 hArg    have hmul : 1 ≤ (1 / θ ^ 2) * θ := by      have hθ_ne : θ ≠ 0 := hθ_pos.ne'      rw [pow_two]      field_simp [hθ_ne]      linarith    have hcoeff : 1 ≤ (1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A)) := by      calc        1 ≤ (1 / θ ^ 2) * θ := hmul        _ ≤ (1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A)) := by            gcongr    calc      volume (E_lam t) ≤ volume B := measure_mono hsub      _ = ENNReal.ofReal 1 * volume B := by simp      _ ≤ ENNReal.ofReal ((1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A))) * volume B := by          have hcoeff' :              ENNReal.ofReal (1 : ℝ) ≤                ENNReal.ofReal ((1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A))) :=            ENNReal.ofReal_le_ofReal hcoeff          exact mul_le_mul_of_nonneg_right hcoeff' (by positivity)      _ = ENNReal.ofReal (1 / θ ^ 2) * volume B *            ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by          rw [ENNReal.ofReal_mul (by positivity)]          ring