diff --git a/projects/LeanModularForms/.mathlib-quality/learnings.jsonl b/projects/LeanModularForms/.mathlib-quality/learnings.jsonl
new file mode 100644
index 000000000..a166ce986
--- /dev/null
+++ b/projects/LeanModularForms/.mathlib-quality/learnings.jsonl
@@ -0,0 +1,3 @@
+{"type":"style_correction","date":"2026-07-02","file":"Issues/SelfDual/Basic.lean","summary":"Per-declaration cleanup workers cannot catch cross-declaration proof-block duplication; the Phase-6.5 /simplify holistic pass found the `hdualΓ` (strictWidthInfty ∈ (dual Γ).strictPeriods) block copy-pasted across two declarations and extracted it into a shared private helper `strictWidthInfty_mem_dual_strictPeriods`.","lesson":"Always run the holistic simplify pass after per-decl golf; it is where cross-cutting DRY wins surface."}
+{"type":"mathlib_discovery","date":"2026-07-02","file":"Issues/SelfDual/Basic.lean","summary":"`Subgroup.strictWidthInfty` is a bare `dite` on `DiscreteTopology _.strictPeriods` with no congruence lemma, so `Subgroup.dual_width_eq` must reconstruct the def body under `congrArg` (rw/simp fail with 'motive is not type correct' / 'failed to synthesize Decidable'). A `strictWidthInfty_congr (h : Γ₁.strictPeriods = Γ₂.strictPeriods) : strictWidthInfty Γ₁ = strictWidthInfty Γ₂` is the missing API (upstream/dev-ticket candidate)."}
+{"type":"mathlib_discovery","date":"2026-07-03","file":"Issues/Issue34.lean","summary":"To prove a ring hom `σ : IntermediateField ℚ ℂ →+* ℂ` is real on an adjoin (`conjugate σ = σ`), do NOT hand-roll `IntermediateField.adjoin_induction` with per-operation `change`/`rw [map_*, star_*]` closure branches (~22 lines). Instead bundle both ring homs as ℚ-AlgHoms via `RingHom.equivRatAlgHom : (A →+* B) ≃ (A →ₐ[ℚ] B)` and apply `IntermediateField.algHom_ext_of_eq_adjoin (F := ℚ) rfl` (or `adjoin_algHom_ext`), reducing the goal to the generator case (`rintro x ⟨n, rfl⟩; show star (σ ⟨_,_⟩) = σ ⟨_,_⟩; exact Complex.conj_eq_iff_im.mpr (h n)`). ~22 lines → 5.","lesson":"A per-declaration cleanup worker rejected this refactor (feared manual AlgHom bundling); the /simplify holistic pass (3 of 4 angles) found it. `equivRatAlgHom` makes ℚ-linearity free, so the AlgHom ext lemmas apply to any ring hom between ℚ-algebras — the `change`-heavy adjoin_induction is the missing-API smell mathlib warns about."}
diff --git a/projects/LeanModularForms/.mathlib-quality/renames.jsonl b/projects/LeanModularForms/.mathlib-quality/renames.jsonl
new file mode 100644
index 000000000..e69de29bb
diff --git a/projects/LeanModularForms/LeanModularForms/Issues/Example.lean b/projects/LeanModularForms/LeanModularForms/Issues/Example.lean
new file mode 100644
index 000000000..078492785
--- /dev/null
+++ b/projects/LeanModularForms/LeanModularForms/Issues/Example.lean
@@ -0,0 +1,127 @@
+import LeanModularForms.Issues.Issue55
+
+/-!
+# A congruence subgroup that is not self-dual, carrying a self-dual form
+
+This file constructs a concrete example separating three properties of a subgroup of
+`SL(2, ℤ)` and a modular form on it. The subgroup `Γ` is the preimage, modulo `3`, of the
+stabilizer of the line spanned by `(1, 1)`. It is a congruence subgroup but is not self-dual,
+yet the discriminant cusp form `Δ` restricted to it is self-dual.
+
+## Main definitions
+
+* `IssueExample.Γ`: the subgroup of `SL(2, ℤ)` whose reduction mod `3` fixes the sum
+  `γ 0 0 + γ 0 1` and `γ 1 0 + γ 1 1`.
+* `IssueExample.Δ`: the discriminant cusp form restricted from `SL(2, ℤ)` to `Γ`.
+
+## Main results
+
+* `IssueExample.result`: `Γ` is a congruence subgroup, `Γ` is not self-dual, and `Δ` is
+  self-dual.
+-/
+
+open ModularForm UpperHalfPlane MatrixGroups ComplexConjugate
+open CongruenceSubgroup Pointwise Subgroup
+open Matrix Matrix.SpecialLinearGroup Complex
+open scoped MatrixGroups ModularForm Real
+
+private lemma eta_neg_conj (z : UpperHalfPlane) :
+    conj (ModularForm.eta (-(conj (z : ℂ)))) = ModularForm.eta (z : ℂ) := by
+  have hz' : (-(conj (z : ℂ))) ∈ UpperHalfPlane.upperHalfPlaneSet := by
+    simpa using z.2
+  have hprod := (ModularForm.multipliableLocallyUniformlyOn_eta.multipliable hz').map_tprod
+    (starRingEnd ℂ) Complex.continuous_conj
+  rw [ModularForm.eta, map_mul, hprod, ModularForm.eta]
+  simp [ModularForm.eta_q, Function.Periodic.qParam, ← Complex.exp_conj, map_ofNat]
+
+namespace IssueExample
+
+/-- The subgroup of `SL(2, ℤ)` whose reduction modulo `3` stabilizes the line
+spanned by `(1, 1)`. -/
+def Γ : Subgroup SL(2, ℤ) where
+  carrier := {γ | (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3)}
+  one_mem' := by norm_num
+  mul_mem' := by
+    intro A B hA hB
+    change ((A * B) 0 0 + (A * B) 0 1 : ZMod 3) =
+      ((A * B) 1 0 + (A * B) 1 1 : ZMod 3)
+    have hA' : (A 0 0 : ZMod 3) + (A 0 1 : ZMod 3) =
+        (A 1 0 : ZMod 3) + (A 1 1 : ZMod 3) := hA
+    have hB' : (B 0 0 : ZMod 3) + (B 0 1 : ZMod 3) =
+        (B 1 0 : ZMod 3) + (B 1 1 : ZMod 3) := hB
+    simp only [Fin.isValue, Matrix.SpecialLinearGroup.coe_mul, Matrix.mul_apply,
+      Fin.sum_univ_two, Int.cast_add, Int.cast_mul]
+    linear_combination ((B 0 0 : ZMod 3) + (B 0 1 : ZMod 3)) * hA' +
+      ((A 1 1 : ZMod 3) - (A 0 1 : ZMod 3)) * hB'
+  inv_mem' := by
+    intro A hA
+    change ((A⁻¹) 0 0 + (A⁻¹) 0 1 : ZMod 3) =
+      ((A⁻¹) 1 0 + (A⁻¹) 1 1 : ZMod 3)
+    have hA' : (A 0 0 : ZMod 3) + (A 0 1 : ZMod 3) =
+        (A 1 0 : ZMod 3) + (A 1 1 : ZMod 3) := hA
+    rw [SL2_inv_expl A]
+    simp only [Fin.isValue, cons_val', cons_val_zero, cons_val_fin_one, cons_val_one, Int.cast_neg]
+    linear_combination -hA'
+
+theorem mem_Γ (γ : SL(2, ℤ)) : γ ∈ Γ ↔ (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3) :=
+  Iff.rfl
+
+theorem Γ_isCongruenceSubgroup : CongruenceSubgroup.IsCongruenceSubgroup Γ := by
+  refine ⟨3, by norm_num, ?_⟩
+  intro γ hγ
+  rw [CongruenceSubgroup.Gamma_mem] at hγ
+  change (γ 0 0 + γ 0 1 : ZMod 3) = (γ 1 0 + γ 1 1 : ZMod 3)
+  simp [hγ]
+
+theorem Γ_not_isSelfDual :
+    ¬ Subgroup.IsSelfDual (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+  let γ : SL(2, ℤ) := ⟨!![0, 1; -1, -1], by norm_num [Matrix.det_fin_two_of]⟩
+  let γJ : SL(2, ℤ) := ⟨!![0, -1; 1, -1], by norm_num [Matrix.det_fin_two_of]⟩
+  have hγΓ : γ ∈ Γ := by
+    change ((0 : ZMod 3) + (1 : ZMod 3) = (-1 : ZMod 3) + (-1 : ZMod 3))
+    decide
+  have hγJ_not : γJ ∉ Γ := by
+    change ¬ ((0 : ZMod 3) + (-1 : ZMod 3) = (1 : ZMod 3) + (-1 : ZMod 3))
+    decide
+  have hJinv : UpperHalfPlane.J⁻¹ = UpperHalfPlane.J :=
+    inv_eq_of_mul_eq_one_right <| by simpa [sq] using UpperHalfPlane.J_sq
+  have hmapγJ : mapGL ℝ γJ = UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J := by
+    ext i j
+    fin_cases i <;> fin_cases j <;>
+      norm_num [γ, γJ, UpperHalfPlane.J, Matrix.GeneralLinearGroup.coe_mul,
+        Matrix.mul_apply, Matrix.vecMul, dotProduct, Matrix.vecHead, Matrix.vecTail,
+        Fin.sum_univ_two]
+  have hdual_mem : UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J ∈
+      Subgroup.dual (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+    rw [Subgroup.dual, hJinv]
+    simpa [ConjAct.toConjAct_smul, hJinv] using
+      Subgroup.smul_mem_pointwise_smul (mapGL ℝ γ) (ConjAct.toConjAct UpperHalfPlane.J)
+        (Γ : Subgroup (GL (Fin 2) ℝ)) (Subgroup.mem_map.mpr ⟨γ, hγΓ, rfl⟩)
+  have hnot_mem : UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J ∉
+      (Γ : Subgroup (GL (Fin 2) ℝ)) := by
+    intro hmem
+    obtain ⟨δ, hδΓ, hδ⟩ := Subgroup.mem_map.mp hmem
+    have hδ_eq : δ = γJ := mapGL_injective (by rw [hδ, ← hmapγJ])
+    exact hγJ_not (hδ_eq ▸ hδΓ)
+  intro hself
+  exact hnot_mem (by simpa [hself.isSelfDual] using hdual_mem)
+
+theorem Γ_le_SL : (Γ : Subgroup (GL (Fin 2) ℝ)) ≤ 𝒮ℒ := Subgroup.map_le_range (mapGL ℝ) Γ
+
+/-- The discriminant cusp form, restricted from the full modular group to `Γ`. -/
+noncomputable def Δ : CuspForm (Γ : Subgroup (GL (Fin 2) ℝ)) 12 :=
+  CuspForm.restrictSubgroup Γ_le_SL CuspForm.discriminant
+
+theorem Δ_isSelfDual : ModularFormClass.isSelfDual Δ := by
+  ext z
+  rw [ModularFormClass.dual_explicit]
+  change conj (ModularForm.discriminant (ofComplex (-(conj (z : ℂ))))) =
+    ModularForm.discriminant z
+  have hz' : 0 < (-(conj (z : ℂ))).im := by simpa using z.2
+  simp [ModularForm.discriminant, ofComplex_apply_of_im_pos hz', map_pow, eta_neg_conj]
+
+/-- The concrete example: `Γ` is congruence and not self-dual, while `Δ` is self-dual. -/
+theorem result : IsCongruenceSubgroup Γ ∧ ¬ Subgroup.IsSelfDual Γ ∧ ModularFormClass.isSelfDual Δ :=
+  ⟨Γ_isCongruenceSubgroup, Γ_not_isSelfDual, Δ_isSelfDual⟩
+
+end IssueExample
diff --git a/projects/LeanModularForms/LeanModularForms/Issues/Issue34.lean b/projects/LeanModularForms/LeanModularForms/Issues/Issue34.lean
new file mode 100644
index 000000000..eb0a33df6
--- /dev/null
+++ b/projects/LeanModularForms/LeanModularForms/Issues/Issue34.lean
@@ -0,0 +1,99 @@
+import LeanModularForms.Issues.Issue55
+
+open ModularForm UpperHalfPlane MatrixGroups ComplexConjugate CongruenceSubgroup Pointwise Subgroup
+  Matrix.SpecialLinearGroup HeckeRing.GL2
+
+variable {N : ℕ} [NeZero N] {k : ℤ}
+
+namespace HeckeRing.GL2
+
+namespace Newform
+
+/-- The coefficient field `ℚ(a_n : n ≥ 1)` of a newform. -/
+noncomputable def coefficientField (f : Newform N k) : IntermediateField ℚ ℂ :=
+  IntermediateField.adjoin ℚ (Set.range fun n : ℕ+ ↦ (qExpansion 1 f.toCuspForm).coeff n)
+
+/-- The coefficient field of a newform is finite-dimensional over `ℚ`. -/
+theorem coefficientField_finiteDimensional (f : Newform N k) :
+    FiniteDimensional ℚ f.coefficientField := by
+  sorry
+
+/-- The coefficient field of a newform is a number field. -/
+instance (f : Newform N k) : NumberField f.coefficientField :=
+  {to_finiteDimensional := coefficientField_finiteDimensional f}
+
+lemma coeff_mem_coefficientField (f : Newform N k) (n : ℕ+) :
+    (qExpansion 1 f.toCuspForm).coeff n ∈ f.coefficientField :=
+  IntermediateField.subset_adjoin ℚ _ (Set.mem_range_self n)
+
+lemma isSelfDual_iff_qExpansion_one_coeff_im_eq_zero (f : Newform N k) :
+    ModularFormClass.isSelfDual f.toCuspForm ↔
+      ∀ n : ℕ, ((qExpansion 1 f.toCuspForm).coeff n).im = 0 := by
+  simpa [CongruenceSubgroup.strictWidthInfty_Gamma1 N] using
+    ModularFormClass.isSelfDual_iff f.toCuspForm
+
+lemma qExpansion_one_coeff_im_eq_zero_of_coefficientField_isTotallyReal (f : Newform N k)
+    (hK : NumberField.IsTotallyReal f.coefficientField) :
+    ∀ n : ℕ, ((qExpansion 1 f.toCuspForm).coeff n).im = 0 := by
+  intro n
+  cases n with
+  | zero => simp [CuspFormClass.qExpansion_coeff_zero f.toCuspForm one_pos (one_mem_strictPeriods_Gamma1_map N)]
+  | succ n =>
+      let npos : ℕ+ := ⟨n + 1, n.succ_pos⟩
+      simpa [npos] using Complex.conj_eq_iff_im.mp (RingHom.congr_fun
+        (NumberField.IsTotallyReal.complexEmbedding_isReal (algebraMap f.coefficientField ℂ))
+        ⟨(qExpansion 1 f.toCuspForm).coeff npos, coeff_mem_coefficientField f npos⟩)
+
+/--
+For every embedding σ : K_f ↪ ℂ, the coefficientwise conjugate
+f^σ(q) = ∑ n ≥ 1, σ(a_n(f)) q^n
+is again a normalized newform. Its dual has coefficients
+a_n((f^σ)ᵛ) = overline(σ(a_n(f))).
+Galois conjugation commutes with duality:
+(f^σ)ᵛ = (fᵛ)^σ.
+-/
+theorem exists_selfDual_galoisConjugate_newform_of_isSelfDual (f : Newform N k)
+    (hself : ModularFormClass.isSelfDual f.toCuspForm) (σ : f.coefficientField →+* ℂ) :
+    ∃ g : Newform N k, ModularFormClass.isSelfDual g.toCuspForm ∧
+      ∀ n : ℕ+, (qExpansion 1 g.toCuspForm).coeff n =
+        σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩ := by
+  sorry
+
+lemma complexEmbedding_coeff_im_eq_zero_of_isSelfDual (f : Newform N k)
+    (hself : ModularFormClass.isSelfDual f.toCuspForm) (σ : f.coefficientField →+* ℂ) (n : ℕ+) :
+    (σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩).im = 0 := by
+  obtain ⟨g, hgself, hgcoeff⟩ := exists_selfDual_galoisConjugate_newform_of_isSelfDual f hself σ
+  rw [← hgcoeff n]
+  exact (isSelfDual_iff_qExpansion_one_coeff_im_eq_zero g).mp hgself n
+
+lemma coefficientField_isTotallyReal_of_forall_complexEmbedding_coeff_im_eq_zero
+    (f : Newform N k) (hσ : ∀ (σ : f.coefficientField →+* ℂ) (n : ℕ+),
+      (σ ⟨(qExpansion 1 f.toCuspForm).coeff n, coeff_mem_coefficientField f n⟩).im = 0) :
+    NumberField.IsTotallyReal f.coefficientField := by
+  unfold coefficientField at hσ ⊢
+  refine ⟨fun v ↦ ?_⟩
+  rw [NumberField.InfinitePlace.isReal_iff]
+  let σ := NumberField.InfinitePlace.embedding v
+  rw [NumberField.ComplexEmbedding.isReal_iff]
+  apply RingHom.equivRatAlgHom.injective
+  apply IntermediateField.algHom_ext_of_eq_adjoin (F := ℚ) rfl
+  rintro x ⟨n, rfl⟩
+  change star (σ ⟨_, _⟩) = σ ⟨_, _⟩
+  exact Complex.conj_eq_iff_im.mpr (hσ σ n)
+
+/-- A newform's coefficient field is totally real if and only if the newform is self-dual. -/
+theorem coefficientField_isTotallyReal_iff_isSelfDual (f : Newform N k) :
+    NumberField.IsTotallyReal f.coefficientField ↔ ModularFormClass.isSelfDual f.toCuspForm :=
+  ⟨fun hK ↦ (isSelfDual_iff_qExpansion_one_coeff_im_eq_zero f).mpr
+    (qExpansion_one_coeff_im_eq_zero_of_coefficientField_isTotallyReal f hK),
+    fun hself ↦ coefficientField_isTotallyReal_of_forall_complexEmbedding_coeff_im_eq_zero f
+      (complexEmbedding_coeff_im_eq_zero_of_isSelfDual f hself)⟩
+
+/-- A newform's coefficient field is CM if and only if the newform is not self-dual. -/
+theorem coefficientField_isCM_iff_not_isSelfDual (f : Newform N k) :
+    NumberField.IsCMField f.coefficientField ↔ ¬ ModularFormClass.isSelfDual f.toCuspForm := by
+  sorry
+
+end Newform
+
+end HeckeRing.GL2
diff --git a/projects/LeanModularForms/LeanModularForms/Issues/Issue55.lean b/projects/LeanModularForms/LeanModularForms/Issues/Issue55.lean
new file mode 100644
index 000000000..f289a7ab6
--- /dev/null
+++ b/projects/LeanModularForms/LeanModularForms/Issues/Issue55.lean
@@ -0,0 +1,284 @@
+import Mathlib
+
+import LeanModularForms.HeckeRIngs.GL2.Gamma1Pair
+import LeanModularForms.HeckeRIngs.GL2.Newforms
+
+open ModularForm UpperHalfPlane MatrixGroups ComplexConjugate CongruenceSubgroup Pointwise Subgroup
+
+variable {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}
+
+/-- The dual of a subgroup of `GL (Fin 2) ℝ` is its conjugate by `J⁻¹`. -/
+noncomputable def Subgroup.dual (Γ : Subgroup (GL (Fin 2) ℝ)) : Subgroup (GL (Fin 2) ℝ) :=
+  (ConjAct.toConjAct UpperHalfPlane.J⁻¹) • Γ
+
+private lemma J_mul_self : UpperHalfPlane.J * UpperHalfPlane.J = 1 := by
+  simpa [sq] using UpperHalfPlane.J_sq
+
+private lemma J_inv : UpperHalfPlane.J⁻¹ = UpperHalfPlane.J :=
+  inv_eq_of_mul_eq_one_right J_mul_self
+
+namespace Subgroup
+
+open Matrix.GeneralLinearGroup
+
+/-- Conjugation by `J` sends `upperRightHom x` to `upperRightHom (-x)`. -/
+theorem dual_upperRightHom (x : ℝ) :
+    ConjAct.toConjAct UpperHalfPlane.J • upperRightHom x = upperRightHom (-x) := by
+  rw [ConjAct.toConjAct_smul, J_inv]
+  ext i j
+  fin_cases i <;> fin_cases j <;>
+    norm_num [UpperHalfPlane.J, Matrix.GeneralLinearGroup.upperRightHom, Matrix.mul_apply,
+      Fin.sum_univ_two]
+
+/-- Dualising a subgroup preserves its strict periods. -/
+theorem dual_strictPeriods_eq (Γ : Subgroup (GL (Fin 2) ℝ)) :
+    (Subgroup.dual Γ).strictPeriods = Γ.strictPeriods := by
+  ext x
+  simp only [mem_strictPeriods_iff, Subgroup.dual, mem_pointwise_smul_iff_inv_smul_mem,
+    map_inv, inv_inv, dual_upperRightHom]
+  simpa using (Subgroup.inv_mem_iff Γ (x := upperRightHom x))
+
+end Subgroup
+
+/-- A subgroup is self-dual when it equals its own dual. -/
+class Subgroup.IsSelfDual (Γ : Subgroup (GL (Fin 2) ℝ)) : Prop where
+  isSelfDual : Subgroup.dual Γ = Γ
+
+/-- Example: the trivial subgroup is self-dual. -/
+instance : Subgroup.IsSelfDual (⊥ : Subgroup (GL (Fin 2) ℝ)) where
+  isSelfDual := by simp [Subgroup.dual]
+
+/-- The dual of a modular-form-like object is its translate by `J`. -/
+noncomputable def ModularFormClass.dual {F : Type*} [FunLike F UpperHalfPlane ℂ]
+    [ModularFormClass F Γ k] (f : F) : ModularForm (Subgroup.dual Γ) k :=
+  ModularForm.translate f UpperHalfPlane.J
+
+/-- A modular-form-like object is self-dual when it equals its own dual. -/
+def ModularFormClass.isSelfDual {F : Type*} [FunLike F UpperHalfPlane ℂ]
+    [ModularFormClass F Γ k] (f : F) : Prop :=
+  ⇑(ModularFormClass.dual f) = ⇑f
+
+/-- Transporting a modular form along an equality of subgroups leaves its coercion unchanged. -/
+theorem ModularForm.coe_cast_group {Γ Γ' : Subgroup (GL (Fin 2) ℝ)}
+    (h : Γ = Γ') (f : ModularForm Γ k) : ⇑(h ▸ f : ModularForm Γ' k) = ⇑f := by
+  cases h
+  rfl
+
+open Classical in
+/-- Dualising a subgroup preserves the strict width of the cusp `∞`. -/
+theorem Subgroup.dual_width_eq (Γ : Subgroup (GL (Fin 2) ℝ)) :
+    strictWidthInfty (Subgroup.dual Γ) = strictWidthInfty Γ :=
+  congrArg (fun H : AddSubgroup ℝ ↦
+    if h : DiscreteTopology H then
+      |Exists.choose <| H.isAddCyclic_iff_exists_zmultiples_eq_top.mp
+        <| AddSubgroup.discrete_iff_addCyclic.mpr h|
+    else 0) (Subgroup.dual_strictPeriods_eq Γ)
+
+private lemma strictWidthInfty_mem_dual_strictPeriods (Γ : Subgroup (GL (Fin 2) ℝ))
+    [Γ.IsArithmetic] : strictWidthInfty Γ ∈ (Subgroup.dual Γ).strictPeriods := by
+  rw [← Subgroup.dual_width_eq Γ]
+  exact (Subgroup.dual Γ).strictWidthInfty_mem_strictPeriods
+
+private lemma qParam_J_smul (h : ℝ) (z : UpperHalfPlane) :
+    Function.Periodic.qParam h ((UpperHalfPlane.J • z : UpperHalfPlane) : ℂ) =
+      conj (Function.Periodic.qParam h (z : ℂ)) := by
+  simp [Function.Periodic.qParam, UpperHalfPlane.coe_J_smul, ← Complex.exp_conj, map_ofNat]
+
+/-- `f.dual` at `z` equals the complex conjugate of `f` at `ofComplex (-conj z)`. -/
+theorem ModularFormClass.dual_explicit {F : Type*} [FunLike F UpperHalfPlane ℂ]
+    [ModularFormClass F Γ k] (f : F) (z : UpperHalfPlane) :
+    ModularFormClass.dual f z = conj (f (ofComplex (-(conj (z : ℂ))))) := by
+  change (⇑(f : ModularForm Γ k) ∣[(k : ℤ)] UpperHalfPlane.J) z =
+    conj (f (ofComplex (-(conj (z : ℂ)))))
+  simp [ModularForm.slash_apply, UpperHalfPlane.J_smul]
+
+private lemma hasSum_qExpansion_dual [Γ.IsArithmetic] {F : Type*} [FunLike F UpperHalfPlane ℂ]
+    [ModularFormClass F Γ k] (f : F) (z : UpperHalfPlane) :
+    HasSum (fun m : ℕ ↦ conj ((qExpansion (strictWidthInfty Γ) f).coeff m) •
+        Function.Periodic.qParam (strictWidthInfty Γ) (z : ℂ) ^ m)
+      (ModularFormClass.dual f z) := by
+  have hf : HasSum (fun m : ℕ ↦ (qExpansion (strictWidthInfty Γ) f).coeff m •
+      Function.Periodic.qParam (strictWidthInfty Γ)
+        ((UpperHalfPlane.J • z : UpperHalfPlane) : ℂ) ^ m) (f (UpperHalfPlane.J • z)) :=
+    UpperHalfPlane.hasSum_qExpansion Γ.strictWidthInfty_pos
+      (SlashInvariantFormClass.periodic_comp_ofComplex f Γ.strictWidthInfty_mem_strictPeriods)
+      (ModularFormClass.holo f) (ModularFormClass.bdd_at_infty f) (UpperHalfPlane.J • z)
+  convert (Complex.hasSum_conj' (f := fun m : ℕ ↦
+    (qExpansion (strictWidthInfty Γ) f).coeff m • Function.Periodic.qParam (strictWidthInfty Γ)
+      ((UpperHalfPlane.J • z : UpperHalfPlane) : ℂ) ^ m)
+    (x := f (UpperHalfPlane.J • z))).mpr hf using 1
+  · ext m
+    simp [qParam_J_smul, smul_eq_mul]
+  · simp [ModularFormClass.dual_explicit, UpperHalfPlane.J_smul]
+
+/-- The `q`-expansion coefficients of the dual are the complex conjugates of the original's. -/
+theorem ModularFormClass.qExpansion_dual_coefficient [Γ.IsArithmetic] {F : Type*}
+    [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) (n : ℕ) :
+    (qExpansion (strictWidthInfty Γ) (ModularFormClass.dual f)).coeff n =
+      conj ((qExpansion (strictWidthInfty Γ) f).coeff n) :=
+  (ModularFormClass.qExpansion_coeff_unique (Γ := Subgroup.dual Γ)
+    (c := fun m : ℕ ↦ conj ((qExpansion (strictWidthInfty Γ) f).coeff m))
+    Γ.strictWidthInfty_pos (strictWidthInfty_mem_dual_strictPeriods Γ)
+    (hasSum_qExpansion_dual f) n).symm
+
+private lemma im_coeff_eq_zero_of_isSelfDual [Γ.IsArithmetic] {F : Type*}
+    [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F)
+    (hself : ModularFormClass.isSelfDual f) (n : ℕ) :
+    ((qExpansion (strictWidthInfty Γ) f).coeff n).im = 0 := by
+  have hcoeff : (qExpansion (strictWidthInfty Γ) (ModularFormClass.dual f)).coeff n =
+      conj ((qExpansion (strictWidthInfty Γ) f).coeff n) :=
+    ModularFormClass.qExpansion_dual_coefficient f n
+  have hsame : (qExpansion (strictWidthInfty Γ) (ModularFormClass.dual f)).coeff n =
+      (qExpansion (strictWidthInfty Γ) f).coeff n := by
+    simpa [ModularFormClass.isSelfDual] using
+      congrArg (fun g : UpperHalfPlane → ℂ ↦ (qExpansion (strictWidthInfty Γ) g).coeff n) hself
+  rw [hsame] at hcoeff
+  exact Complex.conj_eq_iff_im.mp hcoeff.symm
+
+private lemma isSelfDual_of_forall_im_coeff_eq_zero [Γ.IsArithmetic] {F : Type*}
+    [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F)
+    (hreal : ∀ n, ((qExpansion (strictWidthInfty Γ) f).coeff n).im = 0) :
+    ModularFormClass.isSelfDual f := by
+  have hh : 0 < strictWidthInfty Γ := Γ.strictWidthInfty_pos
+  have hΓ : strictWidthInfty Γ ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
+  have hdualΓ : strictWidthInfty Γ ∈ (Subgroup.dual Γ).strictPeriods :=
+    strictWidthInfty_mem_dual_strictPeriods Γ
+  have hqeq : qExpansion (strictWidthInfty Γ) (ModularFormClass.dual f) =
+      qExpansion (strictWidthInfty Γ) f := by
+    ext n
+    exact (ModularFormClass.qExpansion_dual_coefficient f n).trans
+      (Complex.conj_eq_iff_im.mpr (hreal n))
+  have hqsub :
+      qExpansion (strictWidthInfty Γ)
+        (⇑(ModularFormClass.dual f) - ⇑f : UpperHalfPlane → ℂ) = 0 := by
+    rw [UpperHalfPlane.qExpansion_sub
+      (ModularFormClass.analyticAt_cuspFunction_zero (ModularFormClass.dual f) hh hdualΓ)
+      (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ), hqeq, sub_self]
+  have hper : Function.Periodic
+      ((⇑(ModularFormClass.dual f) - ⇑f : UpperHalfPlane → ℂ) ∘ ofComplex)
+        (strictWidthInfty Γ) := by
+    intro z
+    simpa only [Function.comp_apply, Pi.sub_apply] using
+      congrArg₂ (fun a b : ℂ ↦ a - b)
+        (SlashInvariantFormClass.periodic_comp_ofComplex (ModularFormClass.dual f) hdualΓ z)
+        (SlashInvariantFormClass.periodic_comp_ofComplex f hΓ z)
+  have hbdd : IsBoundedAtImInfty
+      (⇑(ModularFormClass.dual f) - ⇑f : UpperHalfPlane → ℂ) := by
+    have : Fact (IsCusp OnePoint.infty (Subgroup.dual Γ)) :=
+      ⟨(Subgroup.dual Γ).isCusp_of_mem_strictPeriods hh hdualΓ⟩
+    change Filter.BoundedAtFilter UpperHalfPlane.atImInfty
+      (⇑(ModularFormClass.dual f) - ⇑f : UpperHalfPlane → ℂ)
+    simpa [sub_eq_add_neg] using
+      (ModularFormClass.bdd_at_infty (ModularFormClass.dual f)).add
+        (ModularFormClass.bdd_at_infty f).neg
+  have hzero : (⇑(ModularFormClass.dual f) - ⇑f : UpperHalfPlane → ℂ) = 0 :=
+    (UpperHalfPlane.qExpansion_eq_zero_iff hh hper
+      ((ModularFormClass.holo (ModularFormClass.dual f)).sub (ModularFormClass.holo f))
+      hbdd).mp hqsub
+  exact funext fun z ↦ sub_eq_zero.mp (congrFun hzero z)
+
+/-- A modular-form-like object is self-dual iff all its `q`-expansion coefficients are real. -/
+theorem ModularFormClass.isSelfDual_iff [Γ.IsArithmetic] {F : Type*}
+    [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) :
+    ModularFormClass.isSelfDual f ↔
+      ∀ n, ((qExpansion (strictWidthInfty Γ) f).coeff n).im = 0 :=
+  ⟨im_coeff_eq_zero_of_isSelfDual f, isSelfDual_of_forall_im_coeff_eq_zero f⟩
+
+section Nebentypus
+
+open Matrix.SpecialLinearGroup HeckeRing.GL2
+
+abbrev Γ₁ (N : ℕ) : Subgroup (GL (Fin 2) ℝ) := (Gamma1 N).map (mapGL ℝ)
+
+private def conjugateByJ (γ : SL(2, ℤ)) : SL(2, ℤ) where
+  val := !![γ 0 0, -γ 0 1; -γ 1 0, γ 1 1]
+  property := by
+    have hdet : γ.val.det = 1 := γ.property
+    rw [Matrix.det_fin_two] at hdet
+    simpa [Matrix.det_fin_two] using hdet
+
+private lemma conjugateByJ_mem_Gamma1_iff (γ : SL(2, ℤ)) :
+    conjugateByJ γ ∈ Gamma1 N ↔ γ ∈ Gamma1 N := by
+  rw [Gamma1_mem, Gamma1_mem]
+  simp [conjugateByJ]
+
+private lemma conjugateByJ_mem_Gamma0 {γ : SL(2, ℤ)} (hγ : γ ∈ Gamma0 N) :
+    conjugateByJ γ ∈ Gamma0 N := by
+  rw [Gamma0_mem] at hγ ⊢
+  simpa [conjugateByJ] using hγ
+
+private lemma Gamma0MapUnits_conjugateByJ (γ : ↥(Gamma0 N)) :
+    Gamma0MapUnits (⟨conjugateByJ (γ : SL(2, ℤ)), conjugateByJ_mem_Gamma0 (N := N) γ.property⟩ :
+    ↥(Gamma0 N)) = Gamma0MapUnits γ := by
+  ext
+  simp [Gamma0MapUnits_val, Gamma0Map, conjugateByJ]
+
+private lemma mapGL_conjugateByJ (γ : SL(2, ℤ)) :
+    mapGL ℝ (conjugateByJ γ) = UpperHalfPlane.J * mapGL ℝ γ * UpperHalfPlane.J := by
+  ext i j
+  fin_cases i <;> fin_cases j <;>
+    norm_num [conjugateByJ, UpperHalfPlane.J, Matrix.GeneralLinearGroup.coe_mul,
+      Matrix.mul_apply, Matrix.vecMul, dotProduct, Matrix.vecHead, Matrix.vecTail,
+      Fin.sum_univ_two]
+
+private lemma J_mul_mapGL_eq_mapGL_conjugateByJ_mul_J (γ : SL(2, ℤ)) :
+    UpperHalfPlane.J * mapGL ℝ γ = mapGL ℝ (conjugateByJ γ) * UpperHalfPlane.J := by
+  rw [mapGL_conjugateByJ, mul_assoc, mul_assoc, J_mul_self, mul_one]
+
+/-- `Γ₁(N)`, viewed inside `GL(2, ℝ)`, is self-dual. -/
+instance CongruenceSubgroup.isSelfDual_Gamma1_map (N : ℕ) :
+    Subgroup.IsSelfDual (Γ₁ N) where
+  isSelfDual := by
+    rw [Subgroup.dual, Γ₁]
+    ext y
+    simp only [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ConjAct.smul_def,
+      ConjAct.ofConjAct_toConjAct, map_inv, inv_inv, Subgroup.mem_map]
+    constructor
+    · rintro ⟨σ, hσ, hσy⟩
+      refine ⟨conjugateByJ σ, (conjugateByJ_mem_Gamma1_iff (N := N) σ).mpr hσ, ?_⟩
+      rw [mapGL_conjugateByJ, hσy, J_inv]
+      calc
+      _ = (UpperHalfPlane.J * UpperHalfPlane.J) * y * (UpperHalfPlane.J * UpperHalfPlane.J) := by group
+      _ = y := by simp [J_mul_self]
+    · rintro ⟨σ, hσ, rfl⟩
+      refine ⟨conjugateByJ σ, (conjugateByJ_mem_Gamma1_iff (N := N) σ).mpr hσ, ?_⟩
+      rw [mapGL_conjugateByJ]
+      simp [J_inv]
+
+/-- The complex conjugate of a `ℂˣ`-valued character. -/
+def MonoidHom.conjChar {G : Type*} [Monoid G] (χ : G →* ℂˣ) : G →* ℂˣ :=
+  (Units.map (starRingEnd ℂ).toMonoidHom).comp χ
+
+/-- Conjugating a character twice recovers the original. -/
+@[simp]
+theorem MonoidHom.conjChar_conjChar {G : Type*} [Monoid G] (χ : G →* ℂˣ) :
+    MonoidHom.conjChar (MonoidHom.conjChar χ) = χ := by
+  ext g
+  simp [MonoidHom.conjChar]
+
+namespace ModularFormClass
+
+/-- The dual of a modular form with nebentypus `χ` has nebentypus the conjugate character. -/
+theorem dual_mem_range_modFormCharSpace_inclusion_conjChar {N : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ)
+    (f : modFormCharSpace (N := N) k χ) : ((Subgroup.IsSelfDual.isSelfDual (Γ := Γ₁ N) ▸ ModularFormClass.dual
+    (f : ModularForm (Γ₁ N) k) : ModularForm (Γ₁ N) k)) ∈ modFormCharSpace (N := N) k (MonoidHom.conjChar χ) := by
+  let F : ModularForm (Γ₁ N) k := (Subgroup.IsSelfDual.isSelfDual (Γ := Γ₁ N) ▸
+    ModularFormClass.dual (f : ModularForm (Γ₁ N) k))
+  change F ∈ modFormCharSpace (N := N) k (MonoidHom.conjChar χ)
+  rw [modFormCharSpace_iff_nebentypus]
+  intro γ
+  let γJ : ↥(Gamma0 N) := ⟨conjugateByJ (γ : SL(2, ℤ)), conjugateByJ_mem_Gamma0 (N := N) γ.property⟩
+  have hf := (modFormCharSpace_iff_nebentypus k χ (f : ModularForm (Γ₁ N) k)).mp f.property γJ
+  have hF : ⇑F = ⇑(ModularFormClass.dual (f : ModularForm (Γ₁ N) k)) :=
+    ModularForm.coe_cast_group _ _
+  rw [hF]
+  change (⇑(f : ModularForm (Γ₁ N) k) ∣[k] UpperHalfPlane.J) ∣[k]
+      (mapGL ℝ (γ : SL(2, ℤ))) = (↑(MonoidHom.conjChar χ (Gamma0MapUnits γ)) : ℂ) •
+      (⇑(f : ModularForm (Γ₁ N) k) ∣[k] UpperHalfPlane.J)
+  rw [← SlashAction.slash_mul, J_mul_mapGL_eq_mapGL_conjugateByJ_mul_J,
+    SlashAction.slash_mul, hf, Gamma0MapUnits_conjugateByJ, ModularForm.smul_slash]
+  simp [MonoidHom.conjChar]
+
+end ModularFormClass
+
+end Nebentypus