Basic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

136 declarations, 0 contain sorry, 0 declared as axioms

Definition of automorphic forms on a totally definite quaternion algebra

Main definitions

In the TotallyDefiniteQuaternionAlgebra namespace:

WeightTwoAutomorphicForm F D R -- weight 2 R-valued automorphic forms for the totally definite quaternion algebra D over the totally real field F. Defined as locally-constant functions φ : Dˣ \ (D ⊗ 𝔸_F^∞)ˣ → R which are right-invariant by some compact open subgroup (i.e. ∃ U_φ such that φ(gu)=φ(g) for all u ∈ U) and have trivial central character (i.e. φ(zg)=φ(g) for all z ∈ (𝔸_F^∞)ˣ).
LevelStruct F R: A structure containing a compact open and a character on it.
LevelStruct.form ℒ D: The submodule S(U, χ) of WeightTwoAutomorphicForm F D R.
LocalLevelStruct F R: A structure containing a compact open and a character on it.

Imports (9)

Imported by 2 files

lemma TotallyDefiniteQuaternionAlgebra.range_unitsMap_finiteAdeleRing_le_center line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, LE.le, Subgroup, Units, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, MonoidHom.range, Units.map, Algebra.algebraMap, Subgroup.center
Proof uses: Membership.mem, Eq, MonoidHom, of_eq_true, Eq.trans, HMul.hMul, True, forall_congr, RingHom, congrArg, Algebra.commutes, eq_self, implies_true
55 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.(instance at line 96) line 96 source
instance TotallyDefiniteQuaternionAlgebra.(instance at line 97) line 97 source
abbrev TotallyDefiniteQuaternionAlgebra.Dfx Dfx is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$ line 100 source
Source documentation
Dfx is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra
Proof uses: Units, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers
18 instances, coercions and auxiliary constants left out.
```
abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ
…
```
structure TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm This definition is made in mathlib-generality but is not the definition of a weight 2 automorphic form unless Dˣ is compact mod centre at infinity line 109 source
Source documentation
This definition is made in mathlib-generality but is not the definition of a weight 2 automorphic form unless Dˣ is compact mod centre at infinity. This hypothesis will be true if D is a totally definite quaternion algebra over a totally real field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommMonoid
3 instances, coercions and auxiliary constants left out.
```
structure WeightTwoAutomorphicForm
  -- defined over R
  (R : Type*) [AddCommMonoid R] where
…
```
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 129) line 129 source
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq
Proof uses: Units, HMul.hMul, Matrix, MonoidHom, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, Exists, Subgroup, And, IsOpen, Membership.mem, HSMul.hSMul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, Eq.mpr, id, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk.injEq, funext, Eq.symm, Eq.refl
66 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.left_invt' line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl and 2 more
Proof uses: MonoidHom, Subtype.mk, Eq.rec, Exists.intro, of_eq_true, Eq.refl, Eq.trans, True, congrFun', congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.left_invt, eq_self
56 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.trivial_central_char' line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Units, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Eq, HMul.hMul, Matrix, MonoidHom, Units.map, Algebra.algebraMap
Proof uses: Eq.mpr, HSMul.hSMul, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, AddCommMonoid, Units.ext, of_eq_true, RingHom, Eq.trans, True, congrArg, Algebra.smul_def, eq_self, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.trivial_central_char
77 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.trivial_central_char_right line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Units, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Eq, HMul.hMul, Matrix, MonoidHom, Units.map, Algebra.algebraMap
Proof uses: Eq.mpr, id, congrArg, Eq.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.trivial_central_char', AddCommMonoid, Eq.rec, Eq.refl, Units.ext, of_eq_true, RingHom, Eq.trans, True, Algebra.commutes, eq_self
60 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.zero The zero automorphic form for a totally definite quaterion algebra line 156 source
Source documentation
The zero automorphic form for a totally definite quaterion algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, OfNat.ofNat, Matrix.GeneralLinearGroup, Fin, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Units
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def zero : (WeightTwoAutomorphicForm F D R) where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 165) line 165 source
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.zero_apply line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: rfl
39 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.neg Negation on the space of automorphic forms over a totally definite quaternion algebra line 172 source
Source documentation
Negation on the space of automorphic forms over a totally definite quaternion algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Neg.neg, Units
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def neg (φ : WeightTwoAutomorphicForm F D R) : WeightTwoAutomorphicForm F D R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 180) line 180 source
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.neg_apply line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Neg.neg
Proof uses: rfl
37 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.add Addition on the space of automorphic forms over a totally definite quaternion algebra line 188 source
Source documentation
Addition on the space of automorphic forms over a totally definite quaternion algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, HAdd.hAdd
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def add (φ ψ : WeightTwoAutomorphicForm F D R) : WeightTwoAutomorphicForm F D R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 198) line 198 source
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.add_apply line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, HAdd.hAdd
Proof uses: rfl
38 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: AddCommGroup.mk, AddGroup.mk, SubNegMonoid.mk, AddMonoid.mk, Zero.mk, OfNat.ofNat, Add.mk, HAdd.hAdd, NSMul.mk, nsmulRec, Neg.mk, Neg.neg, Sub.mk, SubNegMonoid.sub', ZSMul.mk, zsmulRec
24 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finsetSum_toFun line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, Finset, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Finset.sum
Proof uses: Finset.induction, Classical.propDecidable, id, EmptyCollection.emptyCollection, Eq.refl, Not, Membership.mem, of_eq_true, Insert.insert, Eq.trans, HAdd.hAdd, True, congr, congrArg, Finset.sum_insert, False, eq_false, not_false_eq_true, eq_self
49 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.groupSMul The adelic group action on the space of automorphic forms over a totally definite quaternion algebra line 230 source
Source documentation
The adelic group action on the space of automorphic forms over a totally definite quaternion algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, HMul.hMul, Matrix, Units
36 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
def groupSMul (g : GL₂(𝔸ᶠ[F])) (φ : WeightTwoAutomorphicForm F D R) :
    WeightTwoAutomorphicForm F D R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 245) line 245 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.groupSMul_apply line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Eq, HSMul.hSMul, HMul.hMul, Matrix
Proof uses: rfl
38 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.unitsMap_smul line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Units, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, HSMul.hSMul, Matrix, Fin, OfNat.ofNat, Nat, MonoidHom, Units.map, Algebra.algebraMap
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, Matrix.GeneralLinearGroup, of_eq_true, Eq.trans, True, congrFun', congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.trivial_central_char_right, eq_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mulAction line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, MulAction, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Matrix
Proof uses: MulAction.mk, SemigroupAction.mk, SMul.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.groupSMul
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.distribMulAction line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, DistribMulAction, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Matrix
Proof uses: MulAction, DistribMulAction.mk
45 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.isOpen_stabilizer line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, MulAction.stabilizer
Proof uses: Exists, And, Membership.mem, Eq, HMul.hMul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.right_invt, Subgroup.isOpen_mono, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, HSMul.hSMul
78 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 279) line 279 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.adicCompletion_smul_def line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Eq, HSMul.hSMul, Matrix, IsDedekindDomain.FiniteAdeleRing, MonoidHom, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl
Proof uses: rfl
63 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.IsDedekindDomain.FiniteAdeleRing.toAdicCompletion_apply line 286 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.FiniteAdeleRing.coe_zero line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Eq, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing, OfNat.ofNat
Proof uses: rfl
28 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.unitsMap_adicCompletion_smul line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AddCommGroup, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, HSMul.hSMul, Matrix, Fin, OfNat.ofNat, Nat, MonoidHom, Units.map, Algebra.algebraMap
Proof uses: Eq.mpr, IsDedekindDomain.FiniteAdeleRing, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.mulSingleHom, Classical.propDecidable, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext, Matrix.GeneralLinearGroup, id, AddCommMonoid, Eq.rec, HMul.hMul, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl and 38 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ringSMul The scalar action on the space of weight 2 automorphic forms on a totally definite quaternion algebra line 321 source
Source documentation
The scalar action on the space of weight 2 automorphic forms on a totally definite quaternion algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Semiring, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, HSMul.hSMul, Units
34 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def ringSMul (r : S) (φ : WeightTwoAutomorphicForm F D M) :
    WeightTwoAutomorphicForm F D M where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 331) line 331 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.smul_apply line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Semiring, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, HSMul.hSMul
Proof uses: rfl
45 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.module line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Semiring, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: Module.mk, DistribMulAction.mk, MulAction.mk, SemigroupAction.mk
20 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 347) line 347 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 350) line 350 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 352) line 352 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 356) line 356 source
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mapₗ Mapping an automorphic form along a linear map line 361 source
Source documentation
Mapping an automorphic form along a linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, LinearMap, RingHom.id, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: LinearMap.mk, AddHom.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk, Function.comp, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers
37 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
def mapₗ {N : Type*} [AddCommGroup N] [Module R N] (φ : M →ₗ[R] N) :
    WeightTwoAutomorphicForm F D M →ₗ[R] WeightTwoAutomorphicForm F D N where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.(instance at line 384) line 384 source
structure TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct The structure of an compact open U, and a continuous character on U that is trivial on 𝔸ᶠˣ line 397 source
Source documentation
The structure of an compact open U, and a continuous character on U that is trivial on 𝔸ᶠˣ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing
```
structure LevelStruct where
…
```
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA U 𝔸ᶠˣ of a LevelStruct line 412 source
Source documentation
U 𝔸ᶠˣ of a LevelStruct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix
Proof uses: Max.max, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom.range, Units, Units.map, Algebra.algebraMap
35 instances, coercions and auxiliary constants left out.
```
abbrev UA : Subgroup GL₂(𝔸ᶠ[F]) := ℒ.U ⊔ 𝔸ˣ F
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA The character extended onto U 𝔸ᶠˣ line 415 source
Source documentation
The character extended onto U 𝔸ᶠˣ

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA
Proof uses: Equiv, Prod, Units, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom.range, Units.map, Algebra.algebraMap, LE.le, MonoidHom.ker, Max.max, Subgroup.prodToSupOfRight, MonoidHom.liftOfSurjective', Subtype.mk, MonoidHom.coprod, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
75 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def χA : ℒ.UA →* R :=
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA_inclusion_left line 428 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Eq, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA, Max.max and 7 more
Proof uses: Trans.simple, Prod, Subgroup.prodToSupOfRight, LE.le.trans, Subgroup.center, Subgroup.centralizer, TotallyDefiniteQuaternionAlgebra.range_unitsMap_finiteAdeleRing_le_center, Subgroup.center_le_centralizer, Prod.mk, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Subtype.ext, Units.ext, Matrix.ext, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum and 30 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA_inclusion_right line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, MonoidHom.range, Units, Units.map, Algebra.algebraMap, Eq, MonoidHom and 6 more
Proof uses: Trans.simple, Prod, Subgroup.prodToSupOfRight, LE.le.trans, Subgroup.center, Subgroup.centralizer, TotallyDefiniteQuaternionAlgebra.range_unitsMap_finiteAdeleRing_le_center, Subgroup.center_le_centralizer, Prod.mk, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Subtype.ext, Units.ext, Matrix.ext, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum and 33 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_UA line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA
Proof uses: Subgroup.isOpen_mono, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, le_sup_left, MonoidHom.range, Units, Units.map, Algebra.algebraMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_U
65 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χ line 443 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsOfFinOrder, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
Proof uses: CompactSpace, Iff.mp, IsCompact, Set, isCompact_iff_compactSpace, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isCompact_U, Subgroup.FiniteIndex, MonoidHom.ker, Subgroup.FiniteIndex.of_compactSpace, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_ker, Iff.mpr, Exists, And, LT.lt, Eq, HPow.hPow, isOfFinOrder_iff_pow_eq_one, Exists.intro, Subgroup.index, And.intro and 23 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χA line 454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsOfFinOrder, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA
Proof uses: And, LT.lt, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, HPow.hPow, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Exists, Iff.mp, isOfFinOrder_iff_pow_eq_one, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χ, Iff.mpr, Exists.intro, And.intro, MonoidHom.ext, Prod, Units, MonoidHom.range, Units.map, Algebra.algebraMap, Max.max and 24 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χ_apply line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, IsOfFinOrder, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
Proof uses: And, LT.lt, Eq, HPow.hPow, Exists, Iff.mp, isOfFinOrder_iff_pow_eq_one, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χ, Iff.mpr, Exists.intro, And.intro, id, congrArg
62 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χA_apply line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, IsOfFinOrder, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA
Proof uses: And, LT.lt, Eq, HPow.hPow, Exists, Iff.mp, isOfFinOrder_iff_pow_eq_one, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χA, Iff.mpr, Exists.intro, And.intro, id, congrArg
62 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ Δ_g := U 𝔸ˣ ∩ g⁻¹ Dˣ g line 475 source
Source documentation
Δ_g := U 𝔸ˣ ∩ g⁻¹ Dˣ g

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Matrix
Proof uses: Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Inv.inv, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl
49 instances, coercions and auxiliary constants left out.
```
def Δ (g : GL₂(𝔸ᶠ[F])) : Subgroup GL₂(𝔸ᶠ[F]) :=
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.range_units_le_range Fˣ ≤ Δ_g line 479 source
Source documentation
Fˣ ≤ Δ_g

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, LE.le, Subgroup, Units, Matrix, MonoidHom.range, Units.map, Algebra.algebraMap and 1 more
Proof uses: Membership.mem, Eq, MonoidHom, And.intro, Set, Submonoid, Subgroup.toSubmonoid, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Inv.inv, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, Subgroup.mem_sup_right, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Exists.intro, of_eq_true, RingHom and 22 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma range_units_le_range (g : GL₂(𝔸ᶠ[F])) : 𝓕ˣ ≤ ℒ.Δ D g := by
…
```
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isFiniteRelIndex_Δ [Δ_g : Fˣ] is finite line 496 source
Source documentation
[Δ_g : Fˣ] is finite. Since g⁻¹ U g is compact open, g⁻¹ U g ⊆ x⁻¹GL₂(∏ 𝒪_{Fᵥ})x for some x. Let 𝒪 := x⁻¹M₂(∏ 𝒪_{Fᵥ})x ∩ D. Then 𝒪 is an order (why?) and Δ_g/Fˣ ↪ 𝒪¹ := { x ∈ 𝒪 | N(x) = 1 }, where the latter is finite because it is discrete and bounded in D ⊗_{ℚ} ℝ = ∏ ℍ (See Lemma 17.7.13 in Voight).

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, NumberField.IsTotallyReal, IsQuaternionAlgebra, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup.IsFiniteRelIndex, Units, Matrix, MonoidHom.range and 3 more
Proof uses: knownin1980s
40 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance isFiniteRelIndex_Δ [NumberField.IsTotallyReal F] [IsQuaternionAlgebra F D]
    [IsQuaternionAlgebra.IsTotallyDefinite F D] (ℒ : LevelStruct F R) (g : GL₂(𝔸ᶠ[F])) :
    Subgroup.IsFiniteRelIndex 𝓕ˣ (ℒ.Δ D g) := by
…
```
Mentions: IsQuaternionAlgebra, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 506) line 506 source
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex The index [U 𝔸ˣ ∩ g⁻¹ Dˣ g : Fˣ] as a function on Dˣ\GL₂(𝔸)/U line 512 source
Source documentation
The index [U 𝔸ˣ ∩ g⁻¹ Dˣ g : Fˣ] as a function on Dˣ\GL₂(𝔸)/U.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA
Proof uses: Quotient.lift, DoubleCoset.setoid, Subgroup.relIndex, Units.map, Algebra.algebraMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ, HasEquiv.Equiv
44 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
def ΔIndex (g : Dˣ＼GL₂(𝔸 F)／ℒ.UA) : ℕ :=
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex_mk line 532 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, DoubleCoset.mk, Matrix, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl and 5 more
Proof uses: rfl
38 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_map_ker line 535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, Subgroup.map, Subtype, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Subgroup.subtype, MonoidHom.ker, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
Proof uses: Topology.IsOpenEmbedding.isOpenMap, Set, IsOpen.isOpenEmbedding_subtypeVal, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_ker
47 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form The subspace of modular forms of a given level line 540 source
Source documentation
The subspace of modular forms of a given level.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Eq, HSMul.hSMul, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Set
58 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def form : Submodule R (WeightTwoAutomorphicForm F D M) where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 548) line 548 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 553) line 553 source
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formSubmodule Should not be used directly line 560 source
Source documentation
Should not be used directly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Semiring, SMulCommClass, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Submodule.mk, Submodule.toAddSubmonoid, Membership.mem, Set, AddSubsemigroup.carrier, AddSubmonoid.toAddSubsemigroup, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
abbrev formSubmodule (S : Type*) [Semiring S] [Module S M] [SMulCommClass R S M] :
    Submodule S (WeightTwoAutomorphicForm F D M) where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkForm A constructor for forms in S(U, χ) line 567 source
Source documentation
A constructor for forms in S(U, χ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Units, Eq, HMul.hMul, Matrix, MonoidHom and 10 more
Proof uses: Subtype.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mk
140 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def mkForm
    (f : GL₂(𝔸ᶠ[F]) → M)
    (left_invt : ∀ d g, f (ιD d * g) = f g)
    (right_invt : ∀ g, ∀ u : ℒ.U, f (g * ↑u) = ℒ.χ u • f g)
    (trivial_central_char : ∀ z : 𝔸ᶠ[𝓞 F, F]ˣ, ∀ g, f (z • g) = f g) :
    ℒ.form D M where
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_mul_coe line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers and 8 more
Proof uses: id, congrArg, Subtype.property
100 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_mul_coe' line 584 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers and 8 more
Proof uses: Prod, Units, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom.range, Units.map, Algebra.algebraMap, Max.max, Subgroup.prodToSupOfRight, LE.le.trans, Subgroup.center, Subgroup.centralizer, TotallyDefiniteQuaternionAlgebra.range_unitsMap_finiteAdeleRing_le_center, Subgroup.center_le_centralizer, Exists, Subgroup.prodToSupOfRight_surjective, Prod.mk, Subtype.mk, Exists.intro, Eq.rec, Eq.refl and 19 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.apply_mul_eq_χA_smul line 590 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers and 8 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_mul_coe', Subtype.mk
69 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 594) line 594 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.coe_smul line 600 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, Semiring, SMulCommClass, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, HSMul.hSMul
Proof uses: rfl
55 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 606) line 606 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 613) line 613 source
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkFormA A constructor for forms in S(U, χ) which instead asks for behaviour on U 𝔸ˣ line 621 source
Source documentation
A constructor for forms in S(U, χ) which instead asks for behaviour on U 𝔸ˣ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Units, Eq, HMul.hMul, Matrix, MonoidHom and 10 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkForm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U
91 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
abbrev mkFormA
    (f : GL₂(𝔸ᶠ[F]) → M)
    (left_invt : ∀ d g, f (ιD d * g) = f g)
    (right_invt : ∀ g, ∀ u : ℒ.UA, f (g * ↑u) = ℒ.χA u • f g) :
    ℒ.form D M :=
…
```
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map Mapping a LevelStruct along a ring hom line 635 source
Source documentation
Mapping a LevelStruct along a ring hom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, RingHom
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isCompact_U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOpen_U, MonoidHom.comp, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
28 instances, coercions and auxiliary constants left out.
```
protected noncomputable abbrev map {R' : Type*} [CommRing R'] (ℒ : LevelStruct F R) (f : R →+* R') :
    LevelStruct F R' where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_map line 642 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, IsScalarTower, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Eq, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule.restrictScalars, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map, Algebra.algebraMap
Proof uses: Submodule.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, HSMul.hSMul, MonoidHom, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subtype.mk, True and 21 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ext line 648 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Eq, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom, Subtype, Membership.mem, MonoidHom.comp, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subgroup.inclusion and 1 more
Proof uses: IsCompact, IsOpen, LE.le, Units, Subgroup.subgroupOf, MonoidHom.range, Units.map, Algebra.algebraMap, MonoidHom.ker, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mk, Eq.rec, Eq.refl
69 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 658) line 658 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_U line 680 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Eq, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct
Proof uses: rfl
43 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_χ line 682 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Eq, MonoidHom, Subtype, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, HSMul.hSMul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, MonoidHom.comp and 7 more
Proof uses: rfl
64 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_χ_apply line 686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, HSMul.hSMul, Eq, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subtype.mk and 8 more
Proof uses: rfl
70 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 690) line 690 source
class TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall A level struct is sufficiently small if the associated character has finite order coprime to [Δ_g : Fˣ] for all g line 711 source
Source documentation
A level struct is sufficiently small if the associated character has finite order coprime to [Δ_g : Fˣ] for all g.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
3 instances, coercions and auxiliary constants left out.
```
class IsSufficientlySmall (ℒ : LevelStruct F R) where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.toConjAct_smul_le_ker_χA line 717 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, LE.le, Subgroup, Subtype, Membership.mem, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA and 11 more
Proof uses: Subgroup.le_ker_of_le_ker_of_coprime_relIndex, orderOf, MonoidHom, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, MonoidHom.ext, HPow.hPow, Prod, Units.map, Algebra.algebraMap, Eq, Max.max, Subgroup.prodToSupOfRight, LE.le.trans, Subgroup.center, Subgroup.centralizer, TotallyDefiniteQuaternionAlgebra.range_unitsMap_finiteAdeleRing_le_center, Subgroup.center_le_centralizer, Exists, Subgroup.prodToSupOfRight_surjective and 31 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA_eq_of_exists_mul_mul_eq line 732 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, Exists and 6 more
Proof uses: IsUnit.mul_right_cancel, Inv.inv, IsUnit.map, Group.isUnit, Eq.mpr, id, congr, congrArg, Eq.trans, mul_inv_cancel, map_one, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.toConjAct_smul_le_ker_χA, Exists.intro, congrFun', map_mul, map_inv, mul_assoc, Eq.mp, Eq.symm, Subgroup.subgroupOf and 12 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquivOfSection Given a section to the projection Dˣ＼GL₂(𝔸ᶠ[F])／U → GL₂(𝔸ᶠ[F]), S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U line 748 source
Source documentation
Given a section to the projection Dˣ＼GL₂(𝔸ᶠ[F])／U → GL₂(𝔸ᶠ[F]), S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Semiring, SMulCommClass, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix and 16 more
Proof uses: LinearEquiv.mk, LinearMap.mk, AddHom.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkFormA, HSMul.hSMul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA, Inv.inv
110 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
def formEquivOfSection (S : Type*) [Semiring S] [Module S M] [SMulCommClass R S M]
    [ℒ.IsSufficientlySmall D]
    (σ : Dˣ＼GL₂(𝔸 F)／ℒ.UA → GL₂(𝔸ᶠ[F])) (δ : GL₂(𝔸ᶠ[F]) → Dˣ)
    (u : GL₂(𝔸ᶠ[F]) → ℒ.UA)
    (H : ∀ g : GL₂(𝔸ᶠ[F]), σ (DoubleCoset.mk 𝓓ˣ ℒ.UA g) = ιD (δ g) * g * u g) :
    ℒ.form D M ≃ₗ[S] ((Dˣ＼GL₂(𝔸 F)／ℒ.UA) → M) where
…
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquiv If U is sufficiently small, S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U line 798 source
Source documentation
If U is sufficiently small, S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Semiring, SMulCommClass, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, LinearEquiv, RingHom.id, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, DoubleCoset.Quotient and 12 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquivOfSection, DoubleCoset.σ, Inv.inv, Exists.choose, Eq, MonoidHom, DoubleCoset.σLeft, Function.comp, DoubleCoset.σRight
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def formEquiv (S : Type*) [Semiring S] [Module S M] [SMulCommClass R S M]
    [ℒ.IsSufficientlySmall D] :
    ℒ.form D M ≃ₗ[S] ((Dˣ＼GL₂(𝔸 F)／ℒ.UA) → M) :=
…
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct A somewhat arbitrarily chosen level of an automorphic form line 813 source
Source documentation
A somewhat arbitrarily chosen level of an automorphic form.
```
def _root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct
    (f : WeightTwoAutomorphicForm F D M) :
    LevelStruct F R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mem_form line 825 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 829) line 829 source
abbrev TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite Actually true for all totally definite quaternion algebra D but the instance is provided elsewhere line 835 source
Source documentation
Actually true for all totally definite quaternion algebra D but the instance is provided elsewhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
Proof uses: Finite, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA
22 instances, coercions and auxiliary constants left out.
```
abbrev IsFinite (ℒ : LevelStruct F R) : Prop := Finite (Dˣ＼GL₂(𝔸 F)／ℒ.UA)
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 837) line 837 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 842) line 842 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 847) line 847 source
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap Mapping automorphic forms of a fixed level along a linear map line 857 source
Source documentation
Mapping automorphic forms of a fixed level along a linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsScalarTower, LinearMap, RingHom.id, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: LinearMap.mk, AddHom.mk, Subtype.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mapₗ, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U
73 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def formMap {S N : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (φ : M →ₗ[S] N) :
    ℒ.form D M →ₗ[S] ℒ.form D N where
…
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr Mapping automorphic forms of a fixed level along a linear equiv line 867 source
Source documentation
Mapping automorphic forms of a fixed level along a linear equiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsScalarTower, LinearEquiv, RingHom.id, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: LinearEquiv.ofLinearMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap, LinearEquiv.symm
58 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def formCongr {S N : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (φ : M ≃ₗ[S] N) :
    ℒ.form D M ≃ₗ[S] ℒ.form D N :=
…
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMapₗ formMap as a linear map line 875 source
Source documentation
formMap as a linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, IsScalarTower, SMulCommClass, LinearMap, RingHom.id, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: LinearMap.mk, AddHom.mk, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap
64 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def formMapₗ {S T N : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [CommRing T] [Module T N] [SMulCommClass R T N] [SMulCommClass S T N] :
    (M →ₗ[S] N) →ₗ[T] (ℒ.form D M →ₗ[S] ℒ.form D N) where
…
```
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensor If U is sufficiently small, then M ⊗ S(U, N) = S(U, M ⊗ N) line 885 source
Source documentation
If U is sufficiently small, then M ⊗ S(U, N) = S(U, M ⊗ N).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, SMulCommClass, IsScalarTower, LinearEquiv, RingHom.id, TensorProduct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule and 1 more
Proof uses: LinearEquiv.ofBijective, TensorProduct.AlgebraTensorModule.lift, LinearMap.comp, LinearMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMapₗ, TensorProduct.AlgebraTensorModule.mk
75 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def formTensor [ℒ.IsSufficientlySmall D] [ℒ.IsFinite D]
    (S T N : Type*) [CommRing T] [Module T M] [SMulCommClass R T M]
    [AddCommGroup N] [Module R N] [CommRing S] [Module S M] [Module S N] [Algebra S T]
    [Algebra R S] [IsScalarTower R S N] [IsScalarTower R S M] [IsScalarTower S T M] :
    M ⊗[S] ℒ.form D N ≃ₗ[T] ℒ.form D (M ⊗[S] N) :=
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensor_tmul_apply line 902 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, SMulCommClass, IsScalarTower, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Matrix.GeneralLinearGroup, Fin and 10 more
Proof uses: rfl
90 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar If U is sufficiently small, then M ⊗ S(U, R) = S(U, M) line 911 source
Source documentation
If U is sufficiently small, then M ⊗ S(U, R) = S(U, M).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, IsScalarTower, LinearEquiv, RingHom.id, TensorProduct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: LinearEquiv.trans, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensor, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr, TensorProduct.AlgebraTensorModule.rid
75 instances, coercions and auxiliary constants left out.
```
def formTensorScalar [ℒ.IsSufficientlySmall D] [ℒ.IsFinite D]
    (S : Type*) [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] :
    M ⊗[R] ℒ.form D R ≃ₗ[S] ℒ.form D M :=
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar_tmul line 916 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, IsScalarTower, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, LinearEquiv, RingHom.id and 6 more
Proof uses: rfl
79 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar_tmul_apply line 922 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite, IsScalarTower, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat and 10 more
Proof uses: rfl
95 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 929) line 929 source
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.restrict Restriction of LevelStruct to an open subset line 939 source
Source documentation
Restriction of LevelStruct to an open subset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, IsOpen, LE.le, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mk, MonoidHom.comp, Subtype, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subgroup.inclusion
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def restrict (ℒ : LevelStruct F R) (U : Subgroup GL₂(𝔸ᶠ[F]))
    (hU : IsOpen (X := GL₂(𝔸ᶠ[F])) U) (hU' : U ≤ ℒ.U) : LevelStruct F R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.restrict_le line 949 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, IsOpen, LE.le, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.restrict
Proof uses: Exists.intro, Eq, MonoidHom, Subtype, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, MonoidHom.comp, Subgroup.inclusion, rfl
54 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 954) line 954 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U_mono line 977 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Monotone, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U
Proof uses: LE.le, Exists
19 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA_mono line 981 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Monotone, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA
Proof uses: LE.le, sup_le_sup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom.range, Units, Units.map, Algebra.algebraMap, Exists, le_rfl
41 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ_mono line 985 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Monotone, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ
Proof uses: LE.le, inf_le_inf, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Inv.inv, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA_mono, le_rfl
59 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map_mono line 989 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, RingHom, Monotone, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map
Proof uses: LE.le, Exists.intro, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Eq, MonoidHom, Subtype, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, MonoidHom.comp, Subgroup.inclusion, Exists, id and 3 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_anti line 994 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, AddCommGroup, Module, Antitone, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: LE.le, Membership.mem, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Eq.rec, MonoidHom, MonoidHom.comp, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ, Subgroup.inclusion, Exists, Eq, HSMul.hSMul and 3 more
64 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inf_U_le line 997 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Min.min
Proof uses: le_inf, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U_mono, inf_le_left, inf_le_right
38 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inf_U_eq_iff line 1000 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Iff, Eq, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Min.min, MonoidHom, Subtype, Membership.mem, MonoidHom.comp and 4 more
Proof uses: Iff.intro, Eq.symm, Eq.mpr, Exists, eq_of_heq, HEq, Eq.refl, HEq.refl, MulOne, funext, outParam, Membership, MulOneClass, SetLike, SubmonoidClass, Group, LE.le, Eq.trans, LE.le.antisymm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inf_U_le and 13 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex_mul_relIndex line 1011 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, HMul.hMul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, DoubleCoset.mk, Matrix, MonoidHom.range and 5 more
Proof uses: Subgroup.relIndex_mul_relIndex, Units.map, Algebra.algebraMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.range_units_le_range, inf_le_inf, Subgroup, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Inv.inv, sup_le_sup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Exists, le_rfl
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.orderOf_χ_dvd line 1017 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, Dvd.dvd, Nat, orderOf, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χ
Proof uses: Iff.mpr, Eq, HPow.hPow, orderOf_dvd_iff_pow_eq_one, MonoidHom.ext, Eq.mpr, Subgroup.inclusion, Exists, id, congrFun', congrArg, MonoidHom.comp, Subtype.mk, Subtype.property, pow_orderOf_eq_one
73 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall.of_le line 1023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall.mk, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, Eq, DoubleCoset.mk, Exists, Nat.Coprime, orderOf, MonoidHom and 21 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1031) line 1031 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1034) line 1034 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1037) line 1037 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.orderOf_map_χ_dvd line 1040 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, RingHom, Dvd.dvd, Nat, orderOf, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map and 1 more
Proof uses: Eq.mpr, Eq, HPow.hPow, id, congrArg, propext, orderOf_dvd_iff_pow_eq_one, MonoidHom.ext, of_eq_true, Eq.trans, True, congrFun', Eq.symm, map_pow, pow_orderOf_eq_one, map_one, eq_self
76 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1047) line 1047 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.smul_le_smul_iff line 1055 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.inv_smul_le_iff line 1059 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.smul_inf line 1064 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1070) line 1070 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Subgroup.isFiniteRelIndex_inf_inf line 1074 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.IsFiniteRelIndex, LE.le, Subgroup.centralizer, Max.max
Proof uses: HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, Quotient.map, QuotientGroup.leftRel, MonoidHom, Subgroup.inclusion, le_sup_left, HasEquiv.Equiv, Iff.mpr, HMul.hMul, Inv.inv, QuotientGroup.leftRel_apply, Subgroup.subtype, Iff.mp, Function.Surjective, Eq, Exists, QuotientGroup.mk_surjective and 22 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1090) line 1090 source
class TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Normal (U, χ) is normal in (U', χ') if U ≤ U' is normal and χ'|_U = χ line 1095 source
Source documentation
(U, χ) is normal in (U', χ') if U ≤ U' is normal and χ'|_U = χ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
class Normal (ℒ ℒ' : LevelStruct F R) : Prop extends (ℒ.U.subgroupOf ℒ'.U).Normal where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1098) line 1098 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.le_normalizer line 1102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Normal, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Subgroup.normalizer
Proof uses: Iff.mp, Subgroup.Normal, Subtype, Membership.mem, Subgroup.subgroupOf, Subgroup.normal_subgroupOf_iff_le_normalizer, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U_mono, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Normal.le, inferInstance
39 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.(instance at line 1106) line 1106 source
structure TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct A way to construct LevelStruct via a family of local level structs on finitely many finite places line 1128 source
Source documentation
A way to construct LevelStruct via a family of local level structs on finitely many finite places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing
```
structure LocalLevelStruct where
…
```
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US line 1147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US
Proof uses: dite, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.S, Classical.propDecidable, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US_of_mem, Not, Eq.rec, IsDedekindDomain.GL2.localFullLevel, IsDedekindDomain.GL2.localFullLevel.isOpen, Eq.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US_eq_of_notMem
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US line 1151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsCompact, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US
Proof uses: dite, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.S, Classical.propDecidable, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US_of_mem, Not, Eq.rec, IsDedekindDomain.GL2.localFullLevel, IsDedekindDomain.GL2.localFullLevel.isCompact, Eq.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US_eq_of_notMem
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct The LevelStruct constructed via a LocalLevelStruct line 1158 source
Source documentation
The LevelStruct constructed via a LocalLevelStruct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mk, Subgroup.mk, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Submonoid.mk, Subsemigroup.mk, Set.ofPred, IsDedekindDomain.HeightOneSpectrum, Membership.mem, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Subgroup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, MonoidHom, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, Finset.prod and 6 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
def toStruct : LevelStruct F R where
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.incl line 1205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, IsDedekindDomain.FiniteAdeleRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct
Proof uses: MonoidHom.codRestrict, MonoidHom.comp, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl, Subgroup.subtype
53 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.χ_incl line 1214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.US, Eq, MonoidHom, IsDedekindDomain.FiniteAdeleRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U and 4 more
Proof uses: Eq.mpr, Finset.prod, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.S, Subtype.mk, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, Subgroup.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, Subgroup.subtype, MonoidHom.comp, id, Eq.refl, congrFun', congrArg, Eq.trans, MonoidHom.codRestrict, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct_χ, MonoidHom.finsetProd_apply, Finset.prod_congr and 21 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.