From d840f50ab07fb0170966e100a11aef6123eaf306 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 11 Dec 2024 08:26:31 +0000 Subject: [PATCH] chore(NumberTheory/ModularForms/JacobiTheta): simplify proof of isBigO_atTop_F_int_zero_sub (#19879) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `have ha' : (a : UnitAddCircle) = 0 ↔ a = 0` can be directly proved by `AddCircle.coe_eq_zero_iff_of_mem_Ico ha`. * That makes the proof small enough that it makes sense to inline it at its use in `simp_rw`. This simplification was found by [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep). --- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean index 4e6f7d202b007..b106e2e0d0de9 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean @@ -249,11 +249,7 @@ lemma isBigO_atTop_F_int_zero_sub (a : UnitAddCircle) : ∃ p, 0 < p ∧ obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_zero_sub ha.1 obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_zero_sub (sub_nonneg.mpr ha.2.le) - have ha' : (a : UnitAddCircle) = 0 ↔ a = 0 := by - rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico (hp := ⟨zero_lt_one' ℝ⟩), QuotientAddGroup.mk_zero] - · rw [zero_add]; exact ha - · simp - simp_rw [ha'] + simp_rw [AddCircle.coe_eq_zero_iff_of_mem_Ico ha] simp_rw [eq_false_intro (by linarith [ha.2] : 1 - a ≠ 0), if_false, sub_zero] at hq' refine ⟨_, lt_min hp hq, ?_⟩ have : (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =ᶠ[atTop]