awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₃ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₄ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
  ¬∃ c > 0,
      ∀ᶠ (x : ℝ) in atTop,
        c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₃ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₄ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬∃ c > 0,
        ∀ᶠ (x : ℝ) in atTop,
          c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₅ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (c : ℝ) (_ : c > 0),
  ∃ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (1 x) < c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₃ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₄ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬∃ c > 0,
        ∀ᶠ (x : ℝ) in atTop,
          c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
refine₅ refine₆ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0),
    ∃ᶠ (x : ℝ) in atTop,
      Norm.norm (E := ℝ) (1 x) < a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₇ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (a_1 : ℝ),
  ∃ b ≥ a_1, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b| : ℝ)
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₃ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₄ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬∃ c > 0,
        ∀ᶠ (x : ℝ) in atTop,
          c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
refine₅ refine₆ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0),
    ∃ᶠ (x : ℝ) in atTop,
      Norm.norm (E := ℝ) (1 x) < a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
refine₇ refine₈ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b : ℝ),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₉ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b c : ℝ)
  (hc :
    ∀ b ≥ c,
      Norm.norm (E := ℝ) (1 b) ≤
        a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
  ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (MeromorphicOn.divisor f univ)⁻) 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
have rw : Eq (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (MeromorphicOn.divisor f univ)⁻ 0 ↔
  AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
Tactic: rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
rw :
  Eq (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (MeromorphicOn.divisor f univ)⁻ 0 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (MeromorphicOn.divisor f univ)⁻) 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
have rw₁ : LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor f univ) ↔
  AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
Tactic: rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
rw :
  Eq (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (MeromorphicOn.divisor f univ)⁻ 0 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₁ :
  LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor f univ) ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (MeromorphicOn.divisor f univ)⁻) 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
have rw₂ : LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor (toMeromorphicNFOn f univ) univ) ↔
  AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
Tactic: rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
rw :
  Eq (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (MeromorphicOn.divisor f univ)⁻ 0 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₁ :
  LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor f univ) ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₂ :
  LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor (toMeromorphicNFOn f univ) univ) ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (MeromorphicOn.divisor f univ)⁻) 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
have rw₃ : AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
Tactic: rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
⊢ locallyFinsupp E ℤ →+ locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ
have h : Subset.{u_1} (α := Set E) (closedBall 0 |r|) univ
Tactic: apply restrictMonoidHom
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
⊢ Subset.{u_1} (α := Set E) (closedBall 0 |r|) univ
have h : ∀ ⦃a : E⦄, Membership.mem (γ := Set E) (closedBall 0 |r|) a → Membership.mem (γ := Set E) univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
⊢ (fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (D₁ + D₂) :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₁ + D₂ : (a : E) → ℤ) 0) : ℝ) * log r) =
    HAdd.hAdd (α := ℝ → ℝ)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
      fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r
have simp : (fun (r : ℝ) ↦
    ∑ᶠ (z : E),
        HAdd.hAdd (α := ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
          log (r * ‖z‖⁻¹) +
      HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r) =
  HAdd.hAdd (α := ℝ → ℝ)
    (fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
    fun (r : ℝ) ↦
    ∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹) +
      (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r
Tactic: simp only [map_add, coe_add, Pi.add_apply, Int.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
⊢ ∑ᶠ (z : E),
        HAdd.hAdd (α := ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
          log (r * ‖z‖⁻¹) +
      HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r)
      r
have this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
Tactic: have {A B C D : ℝ} : A + B + (C + D) = A + C + (B + D) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E),
        HAdd.hAdd (α := ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
          log (r * ‖z‖⁻¹) +
      HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    HAdd.hAdd (α := ℝ)
        (∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹))
        (∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹)) +
      ((↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r + (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r)
have h : ∑ᶠ (z : E),
    HAdd.hAdd (α := ℝ)
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ)
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
      log (r * ‖z‖⁻¹) =
  HAdd.hAdd (α := ℝ)
    (∑ᶠ (z : E),
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (r * ‖z‖⁻¹))
    (∑ᶠ (z : E),
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (r * ‖z‖⁻¹))
Tactic: congr 1