Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions public import Mathlib.Tactic.FinCases

Mapping charge spectra values

i. Overview

In this module we define a function map which takes an additive monoid homomorphism f : 𝓩 β†’+ 𝓩1 and a charge spectra x : ChargeSpectrum 𝓩, and returns the charge x.map f : ChargeSpectrum 𝓩1 obtained by mapping the elements of x by f.

There are various properties which are preserved under this mapping:

    Anomaly cancellation.

    The presence of a specific term in the potential.

    Being complete.

There are some properties which are reflected under this mapping:

    Not being pheno-constrained.

    Not regenerating dangerous Yukawa terms at a given level.

We define the preimage of this mapping within a subset ofFinset S5 S10 of Charges 𝓩 in a computationally efficient way.

ii. Key results

    map : The mapping of charge spectra under an additive monoid homomorphism.

    map_allowsTerm : If a charge spectrum allows a potential term, then so does its mapping.

    map_isPhenoConstrained : If a charge spectrum is pheno-constrained, then so is its mapping.

    map_isComplete_iff : A charge spectrum is complete if and only if its mapping is complete.

    map_yukawaGeneratesDangerousAtLevel : A charge spectrum regenerates dangerous Yukawa terms at a given level then so does its mapping.

    preimageOfFinset : The preimage of a charge spectrum in ofFinset S5 S10 under a mapping.

    preimageOfFinsetCard : The cardinality of the preimage of a charge spectrum in ofFinset S5 S10 under a mapping.

iii. Table of contents

    A. The mapping of charge spectra

      A.1. Mapping the empty charge spectrum gives the empty charge spectrum

      A.2. Mapping of charge spectra obeys composing maps

      A.3. Mapping of charge spectra obeys the identity

      A.4. The charges of a field label commute with mapping of charge spectra

      A.5. Mappings of charge spectra preserve the subset relation

      A.6. Mappings of charge spectra and charges of potential terms

      A.7. Mapping charge spectra of `allowsTermForm

      A.8. Mapping preserves whether a charge spectrum allows a potential term

      A.9. Mapping preserves if a charge spectrum is pheno-constrained

      A.10. Mapping preserves completeness of charge spectra

      A.11. Mapping commutes with charges of Yukawa terms

      A.12. Mapping of charge spectra and regenerating dangerous Yukawa terms

    B. Preimage of a charge spectrum under a mapping

      B.1. preimageOfFinset gives the actual preimage

      B.2. Efficient definition for the cardinality of the preimage

      B.3. Definition for the cardinality equals cardinality of the preimage

iv. References

There are no known references for the material in this module.

@[expose] public section

A. The mapping of charge spectra

Given an additive monoid homomorphisms f : 𝓩 β†’+ 𝓩1, for a charge x : Charges 𝓩, x.map f is the charge of Charges 𝓩1 obtained by mapping the elements of x by f.

def map (f : 𝓩 β†’+ 𝓩1) (x : ChargeSpectrum 𝓩) : ChargeSpectrum 𝓩1 where qHd := f <$> x.qHd qHu := f <$> x.qHu Q5 := x.Q5.image f Q10 := x.Q10.image f
/- ### A.1. Mapping the empty charge spectrum gives the empty charge spectrum -/ @[simp] lemma map_empty (f : 𝓩 β†’+ 𝓩1) : map f (βˆ… : ChargeSpectrum 𝓩) = βˆ… := 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1⊒ map f βˆ… = βˆ… 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1⊒ { qHd := none, qHu := none, Q5 := βˆ…, Q10 := βˆ… } = βˆ… All goals completed! πŸ™

A.2. Mapping of charge spectra obeys composing maps

lemma map_map (f : 𝓩 β†’+ 𝓩1) (g : 𝓩1 β†’+ 𝓩2) (x : ChargeSpectrum 𝓩) : map g (map f x) = map (g.comp f) x := 𝓩:Type𝓩1:Type𝓩2:Typeinst✝⁴:AddCommGroup 𝓩inst✝³:AddCommGroup 𝓩1inst✝²:DecidableEq 𝓩1inst✝¹:AddCommGroup 𝓩2inst✝:DecidableEq 𝓩2f:𝓩 β†’+ 𝓩1g:𝓩1 β†’+ 𝓩2x:ChargeSpectrum π“©βŠ’ map g (map f x) = map (g.comp f) x All goals completed! πŸ™

A.3. Mapping of charge spectra obeys the identity

@[simp] lemma map_id [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) : map (AddMonoidHom.id 𝓩) x = x := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum π“©βŠ’ map (AddMonoidHom.id 𝓩) x = x All goals completed! πŸ™

A.4. The charges of a field label commute with mapping of charge spectra

𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ Finset.image (Neg.neg ∘ ⇑f) Q5 = Finset.image (⇑f) (Finset.map { toFun := Neg.neg, inj' := β‹― } Q5) 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ Finset.image (⇑f) (Finset.map { toFun := Neg.neg, inj' := β‹― } Q5) = Finset.image (Neg.neg ∘ ⇑f) Q5 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ Finset.image (⇑f) (Finset.map { toFun := Neg.neg, inj' := β‹― } Q5) = Finset.image (⇑f ∘ Neg.neg) Q5𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ Finset.image (⇑f ∘ Neg.neg) Q5 = Finset.image (Neg.neg ∘ ⇑f) Q5 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ Finset.image (⇑f) (Finset.map { toFun := Neg.neg, inj' := β‹― } Q5) = Finset.image (⇑f ∘ Neg.neg) Q5 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩a:𝓩1⊒ a ∈ Finset.image (⇑f) (Finset.map { toFun := Neg.neg, inj' := β‹― } Q5) ↔ a ∈ Finset.image (⇑f ∘ Neg.neg) Q5 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ ⇑f ∘ Neg.neg = Neg.neg ∘ ⇑f 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩qHd:Option 𝓩qHu:Option 𝓩Q5:Finset 𝓩Q10:Finset 𝓩a:π“©βŠ’ (⇑f ∘ Neg.neg) a = (Neg.neg ∘ ⇑f) a All goals completed! πŸ™

A.5. Mappings of charge spectra preserve the subset relation

lemma map_subset {f : 𝓩 β†’+ 𝓩1} {x y : ChargeSpectrum 𝓩} (h : x βŠ† y) : map f x βŠ† map f y := 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x βŠ† y⊒ map f x βŠ† map f y 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHd).toFinset βŠ† (Option.map (⇑f) y.qHd).toFinset ∧ (Option.map (⇑f) x.qHu).toFinset βŠ† (Option.map (⇑f) y.qHu).toFinset ∧ Finset.image (⇑f) x.Q5 βŠ† Finset.image (⇑f) y.Q5 ∧ Finset.image (⇑f) x.Q10 βŠ† Finset.image (⇑f) y.Q10 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHd).toFinset βŠ† (Option.map (⇑f) y.qHd).toFinset ∧ (Option.map (⇑f) x.qHu).toFinset βŠ† (Option.map (⇑f) y.qHu).toFinset ∧ Finset.image (⇑f) x.Q5 βŠ† Finset.image (⇑f) y.Q5 ∧ Finset.image (⇑f) x.Q10 βŠ† Finset.image (⇑f) y.Q10 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHd).toFinset βŠ† (Option.map (⇑f) y.qHd).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHu).toFinset βŠ† (Option.map (⇑f) y.qHu).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ Finset.image (⇑f) x.Q5 βŠ† Finset.image (⇑f) y.Q5𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ Finset.image (⇑f) x.Q10 βŠ† Finset.image (⇑f) y.Q10 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHd).toFinset βŠ† (Option.map (⇑f) y.qHd).toFinset match x, y with 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩a:Option 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩b:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩hHd:{ qHd := a, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := a, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := a, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := a, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := a, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd).toFinset βŠ† (Option.map ⇑f { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd).toFinset 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩b:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩hHd:{ qHd := none, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := none, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := none, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := none, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := none, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd).toFinset βŠ† (Option.map ⇑f { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩b:Option 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHd:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd).toFinset βŠ† (Option.map ⇑f { qHd := b, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd).toFinset all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHd:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd).toFinset βŠ† (Option.map ⇑f { qHd := none, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHd:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd).toFinset βŠ† (Option.map ⇑f { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd).toFinset all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHd:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ f val✝¹ = f val✝ all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHu:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝¹, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10hHd:val✝¹ = val✝⊒ f val✝¹ = f val✝ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHu✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHu✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHu:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := some val✝, qHu := qHu✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := some val✝, qHu := qHu✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ f val✝ = f val✝ All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ (Option.map (⇑f) x.qHu).toFinset βŠ† (Option.map (⇑f) y.qHu).toFinset match x, y with 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩a:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩b:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩hHd:{ qHd := qHd✝¹, qHu := a, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := a, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := a, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := a, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := qHd✝¹, qHu := a, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu).toFinset βŠ† (Option.map ⇑f { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu).toFinset 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩b:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩hHd:{ qHd := qHd✝¹, qHu := none, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := none, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := none, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := none, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := qHd✝¹, qHu := none, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu).toFinset βŠ† (Option.map ⇑f { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩b:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu).toFinset βŠ† (Option.map ⇑f { qHd := qHd✝, qHu := b, Q5 := Q5✝, Q10 := Q10✝ }.qHu).toFinset all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu).toFinset βŠ† (Option.map ⇑f { qHd := qHd✝, qHu := none, Q5 := Q5✝, Q10 := Q10✝ }.qHu).toFinset𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ (Option.map ⇑f { qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu).toFinset βŠ† (Option.map ⇑f { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu).toFinset all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethHu:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHu.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHu.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ f val✝¹ = f val✝ all_goals 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝¹:𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝¹, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10hHu:val✝¹ = val✝⊒ f val✝¹ = f val✝ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩qHd✝¹:Option 𝓩Q5✝¹:Finset 𝓩Q10✝¹:Finset 𝓩qHd✝:Option 𝓩Q5✝:Finset 𝓩Q10✝:Finset 𝓩val✝:𝓩hHd:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.qHd.toFinset βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.qHd.toFinsethQ5:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q5 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q5hQ10:{ qHd := qHd✝¹, qHu := some val✝, Q5 := Q5✝¹, Q10 := Q10✝¹ }.Q10 βŠ† { qHd := qHd✝, qHu := some val✝, Q5 := Q5✝, Q10 := Q10✝ }.Q10⊒ f val✝ = f val✝ All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ Finset.image (⇑f) x.Q5 βŠ† Finset.image (⇑f) y.Q5 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩hHd:x.qHd.toFinset βŠ† y.qHd.toFinsethHu:x.qHu.toFinset βŠ† y.qHu.toFinsethQ5:x.Q5 βŠ† y.Q5hQ10:x.Q10 βŠ† y.Q10⊒ Finset.image (⇑f) x.Q10 βŠ† Finset.image (⇑f) y.Q10 All goals completed! πŸ™

A.6. Mappings of charge spectra and charges of potential terms

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinset⊒ ((map f x).ofPotentialTerm' T).toFinset = Finset.image (⇑f) (x.ofPotentialTerm' T).toFinset 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1T:PotentialTermheq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' T).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' T).toFinset 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.ΞΌ).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.ΞΌ).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ²).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ²).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ›).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ›).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W3).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W3).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W4).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W4).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.topYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.topYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.ΞΌ).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.ΞΌ).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ²).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ²).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ›).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ›).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W1).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W2).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W3).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W3).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W4).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W4).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K1).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K2).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.topYukawa).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.topYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ ((map f { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.ΞΌ).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.ΞΌ).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ²).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ²).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ›).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ›).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W1).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W2).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W3).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W3).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W4).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W4).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K1).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K2).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.topYukawa).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.topYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ ((map f { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset = Finset.image (⇑f) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.ΞΌ).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.ΞΌ).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ²).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ²).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ›).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ›).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W3).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W3).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W4).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W4).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.topYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.topYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ ((map f { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.ΞΌ).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.ΞΌ).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ²).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ²).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.Ξ›).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.Ξ›).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W3).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W3).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.W4).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.W4).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K1).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K1).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.K2).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.K2).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.topYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.topYukawa).toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ ((map f { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset = Finset.image (⇑f) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1heq:βˆ€ {W : Type} [inst : AddCommGroup W] [inst_1 : DecidableEq W] (y : ChargeSpectrum W) (S : PotentialTerm), (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinsetQ5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ βˆ….toFinset = Finset.image ⇑f βˆ….toFinset All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ i ∈ Finset.image (⇑f) (x.ofPotentialTerm T).toFinset ↔ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm T) All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm T) ↔ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm' T) 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ (βˆƒ a ∈ x.ofPotentialTerm T, f a = i) ↔ βˆƒ a ∈ x.ofPotentialTerm' T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ (βˆƒ a ∈ x.ofPotentialTerm T, f a = i) β†’ βˆƒ a ∈ x.ofPotentialTerm' T, f a = i𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ (βˆƒ a ∈ x.ofPotentialTerm' T, f a = i) β†’ βˆƒ a ∈ x.ofPotentialTerm T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ (βˆƒ a ∈ x.ofPotentialTerm T, f a = i) β†’ βˆƒ a ∈ x.ofPotentialTerm' T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerma:𝓩h:a ∈ x.ofPotentialTerm Th1:f a = i⊒ βˆƒ a ∈ x.ofPotentialTerm' T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerma:𝓩h:a ∈ x.ofPotentialTerm Th1:f a = i⊒ a ∈ x.ofPotentialTerm' T All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerm⊒ (βˆƒ a ∈ x.ofPotentialTerm' T, f a = i) β†’ βˆƒ a ∈ x.ofPotentialTerm T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerma:𝓩h:a ∈ x.ofPotentialTerm' Th1:f a = i⊒ βˆƒ a ∈ x.ofPotentialTerm T, f a = i 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1i:𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerma:𝓩h:a ∈ x.ofPotentialTerm' Th1:f a = i⊒ a ∈ x.ofPotentialTerm T All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTermi:𝓩1⊒ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm' T) ↔ βˆƒ a ∈ x.ofPotentialTerm' T, f a = i All goals completed! πŸ™

A.7. Mapping charge spectra of `allowsTermForm

lemma allowsTermForm_map {T} {f : 𝓩 β†’+ 𝓩1} {a b c : 𝓩} : (allowsTermForm a b c T).map f = allowsTermForm (f a) (f b) (f c) T := 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩T:PotentialTermf:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c T) = allowsTermForm (f a) (f b) (f c) T 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.ΞΌ) = allowsTermForm (f a) (f b) (f c) PotentialTerm.μ𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.Ξ²) = allowsTermForm (f a) (f b) (f c) PotentialTerm.β𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.Ξ›) = allowsTermForm (f a) (f b) (f c) PotentialTerm.Λ𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.W1) = allowsTermForm (f a) (f b) (f c) PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.W2) = allowsTermForm (f a) (f b) (f c) PotentialTerm.W2𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.W3) = allowsTermForm (f a) (f b) (f c) PotentialTerm.W3𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.W4) = allowsTermForm (f a) (f b) (f c) PotentialTerm.W4𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.K1) = allowsTermForm (f a) (f b) (f c) PotentialTerm.K1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.K2) = allowsTermForm (f a) (f b) (f c) PotentialTerm.K2𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.topYukawa) = allowsTermForm (f a) (f b) (f c) PotentialTerm.topYukawa𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1a:𝓩b:𝓩c:π“©βŠ’ map f (allowsTermForm a b c PotentialTerm.bottomYukawa) = allowsTermForm (f a) (f b) (f c) PotentialTerm.bottomYukawa all_goals All goals completed! πŸ™

A.8. Mapping preserves whether a charge spectrum allows a potential term

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩T:PotentialTerma:𝓩b:𝓩c:𝓩h1:allowsTermForm a b c T βŠ† x⊒ map f (allowsTermForm a b c T) βŠ† map f x All goals completed! πŸ™

A.9. Mapping preserves if a charge spectrum is pheno-constrained

lemma map_isPhenoConstrained (f : 𝓩 β†’+ 𝓩1) {x : ChargeSpectrum 𝓩} (h : x.IsPhenoConstrained) : (map f x).IsPhenoConstrained := 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.IsPhenoConstrained⊒ (map f x).IsPhenoConstrained 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.ΞΌ ∨ x.AllowsTerm PotentialTerm.Ξ² ∨ x.AllowsTerm PotentialTerm.Ξ› ∨ x.AllowsTerm PotentialTerm.W2 ∨ x.AllowsTerm PotentialTerm.W4 ∨ x.AllowsTerm PotentialTerm.K1 ∨ x.AllowsTerm PotentialTerm.K2 ∨ x.AllowsTerm PotentialTerm.W1⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.μ⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.β⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.Ξ›βŠ’ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W2⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W4⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.K1⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.K2⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W1⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.μ⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.β⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.Ξ›βŠ’ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W2⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W4⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.K1⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.K2⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩h:x.AllowsTerm PotentialTerm.W1⊒ (map f x).AllowsTerm PotentialTerm.ΞΌ ∨ (map f x).AllowsTerm PotentialTerm.Ξ² ∨ (map f x).AllowsTerm PotentialTerm.Ξ› ∨ (map f x).AllowsTerm PotentialTerm.W2 ∨ (map f x).AllowsTerm PotentialTerm.W4 ∨ (map f x).AllowsTerm PotentialTerm.K1 ∨ (map f x).AllowsTerm PotentialTerm.K2 ∨ (map f x).AllowsTerm PotentialTerm.W1 All goals completed! πŸ™lemma not_isPhenoConstrained_of_map {f : 𝓩 β†’+ 𝓩1} {x : ChargeSpectrum 𝓩} (h : Β¬ (map f x).IsPhenoConstrained) : Β¬ x.IsPhenoConstrained := fun hn => h (map_isPhenoConstrained f hn)

A.10. Mapping preserves completeness of charge spectra

omit [DecidableEq 𝓩] in lemma map_isComplete_iff {f : 𝓩 β†’+ 𝓩1} {x : ChargeSpectrum 𝓩} : (map f x).IsComplete ↔ x.IsComplete := 𝓩:Type𝓩1:Typeinst✝²:AddCommGroup 𝓩inst✝¹:AddCommGroup 𝓩1inst✝:DecidableEq 𝓩1f:𝓩 β†’+ 𝓩1x:ChargeSpectrum π“©βŠ’ (map f x).IsComplete ↔ x.IsComplete All goals completed! πŸ™

A.11. Mapping commutes with charges of Yukawa terms

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩i:𝓩1⊒ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm' PotentialTerm.topYukawa) ∨ i ∈ Multiset.map (⇑f) (x.ofPotentialTerm' PotentialTerm.bottomYukawa) ↔ i ∈ Finset.image (⇑f) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset ∨ i ∈ Finset.image (⇑f) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩i:𝓩1⊒ i ∈ Finset.image (⇑f) x.ofYukawaTerms.toFinset ↔ i ∈ Multiset.map (⇑f) x.ofYukawaTerms All goals completed! πŸ™

A.12. Mapping of charge spectra and regenerating dangerous Yukawa terms

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩n:β„•ih:((map f x).ofYukawaTermsNSum n).toFinset = Finset.image (⇑f) (x.ofYukawaTermsNSum n).toFinseti:𝓩1a:𝓩a_mem:a ∈ x.ofYukawaTermsNSum nb:𝓩b_mem:b ∈ x.ofYukawaTermsh:f a + f b = i⊒ f b ∈ Multiset.map (⇑f) x.ofYukawaTerms 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩n:β„•ih:((map f x).ofYukawaTermsNSum n).toFinset = Finset.image (⇑f) (x.ofYukawaTermsNSum n).toFinseti:𝓩1a:𝓩a_mem:a ∈ x.ofYukawaTermsNSum nb:𝓩b_mem:b ∈ x.ofYukawaTermsh:f a + f b = i⊒ βˆƒ a ∈ x.ofYukawaTerms, f a = f b All goals completed! πŸ™ All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩n:β„•i:𝓩1⊒ i ∈ Finset.image (⇑f) (x.ofYukawaTermsNSum n).toFinset ↔ i ∈ Multiset.map (⇑f) (x.ofYukawaTermsNSum n) All goals completed! πŸ™lemma map_phenoConstrainingChargesSP_toFinset {f : 𝓩 β†’+ 𝓩1} {x : ChargeSpectrum 𝓩} : (map f x).phenoConstrainingChargesSP.toFinset = x.phenoConstrainingChargesSP.toFinset.image f := 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum π“©βŠ’ (map f x).phenoConstrainingChargesSP.toFinset = Finset.image (⇑f) x.phenoConstrainingChargesSP.toFinset All goals completed! πŸ™π“©:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩n:β„•h:x.YukawaGeneratesDangerousAtLevel n⊒ (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset β‰  βˆ… All goals completed! πŸ™lemma not_yukawaGeneratesDangerousAtLevel_of_map {f : 𝓩 β†’+ 𝓩1} {x : ChargeSpectrum 𝓩} (n : β„•) (h : Β¬ (map f x).YukawaGeneratesDangerousAtLevel n) : Β¬ x.YukawaGeneratesDangerousAtLevel n := fun hn => h (map_yukawaGeneratesDangerousAtLevel f n hn)

B. Preimage of a charge spectrum under a mapping

We give a computationally efficient way of calculating the preimage of a charge s : Charges 𝓩1 in a subset ofFinset S5 S10, and then show it is equal to the actual preimage.

The preimage of a charge Charges 𝓩1 in ofFinset S5 S10 βŠ† Charges 𝓩 under mapping charges through f : 𝓩 β†’+ 𝓩1.

def preimageOfFinset (S5 S10 : Finset 𝓩) (f : 𝓩 β†’+ 𝓩1) (x : ChargeSpectrum 𝓩1) : Finset (ChargeSpectrum 𝓩) := let SHd := (S5.map ⟨Option.some, Option.some_injective π“©βŸ© βˆͺ {none} : Finset (Option 𝓩)).filter fun y => f <$> y = x.qHd let SHu := (S5.map ⟨Option.some, Option.some_injective π“©βŸ© βˆͺ {none} : Finset (Option 𝓩)).filter fun y => f <$> y = x.qHu let SQ5' := S5.filter fun y => f y ∈ x.Q5 let SQ5 : Finset (Finset 𝓩) := SQ5'.powerset.filter fun y => y.image f = x.Q5 let SQ10' := S10.filter fun y => f y ∈ x.Q10 let SQ10 : Finset (Finset 𝓩) := SQ10'.powerset.filter fun y => y.image f = x.Q10 (SHd.product <| SHu.product <| SQ5.product SQ10).map toProd.symm.toEmbedding

B.1. preimageOfFinset gives the actual preimage

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 }.qHd.toFinset βŠ† S5 ∧ { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 }.qHu.toFinset βŠ† S5 ∧ { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 }.Q5 βŠ† S5 ∧ { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 }.Q10 βŠ† S10⊒ (yHd = none ∨ βˆƒ a ∈ S5, some a = yHd) ∧ (yHu = none ∨ βˆƒ a ∈ S5, some a = yHu) ∧ y5 βŠ† {x ∈ S5 | βˆƒ a ∈ y5, f a = f x} ∧ y10 βŠ† {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ (yHd = none ∨ βˆƒ a ∈ S5, some a = yHd) ∧ (yHu = none ∨ βˆƒ a ∈ S5, some a = yHu) ∧ y5 βŠ† {x ∈ S5 | βˆƒ a ∈ y5, f a = f x} ∧ y10 βŠ† {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ yHd = none ∨ βˆƒ a ∈ S5, some a = yHd𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ yHu = none ∨ βˆƒ a ∈ S5, some a = yHu𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ y5 βŠ† {x ∈ S5 | βˆƒ a ∈ y5, f a = f x}𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ y10 βŠ† {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ yHd = none ∨ βˆƒ a ∈ S5, some a = yHd match yHd with 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1a:𝓩h2:(some a).toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ some a = none ∨ βˆƒ a_1 ∈ S5, some a_1 = some a 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1a:𝓩h2:a ∈ S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ some a = none ∨ βˆƒ a_1 ∈ S5, some a_1 = some a All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:none.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ none = none ∨ βˆƒ a ∈ S5, some a = none All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ yHu = none ∨ βˆƒ a ∈ S5, some a = yHu match yHu with 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1a:𝓩h2:yHd.toFinset βŠ† S5 ∧ (some a).toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ some a = none ∨ βˆƒ a_1 ∈ S5, some a_1 = some a 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1a:𝓩h2:yHd.toFinset βŠ† S5 ∧ a ∈ S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ some a = none ∨ βˆƒ a_1 ∈ S5, some a_1 = some a All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ none.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ none = none ∨ βˆƒ a ∈ S5, some a = none All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ y5 βŠ† {x ∈ S5 | βˆƒ a ∈ y5, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ βˆ€ ⦃x : 𝓩⦄, x ∈ y5 β†’ x ∈ {x ∈ S5 | βˆƒ a ∈ y5, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y5⊒ x ∈ {x ∈ S5 | βˆƒ a ∈ y5, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y5⊒ x ∈ S5 ∧ βˆƒ a ∈ y5, f a = f x 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y5⊒ βˆƒ a ∈ y5, f a = f x All goals completed! πŸ™ 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ y10 βŠ† {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10⊒ βˆ€ ⦃x : 𝓩⦄, x ∈ y10 β†’ x ∈ {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y10⊒ x ∈ {x ∈ S10 | βˆƒ a ∈ y10, f a = f x} 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y10⊒ x ∈ S10 ∧ βˆƒ a ∈ y10, f a = f x 𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x✝:ChargeSpectrum 𝓩1y:ChargeSpectrum 𝓩yHd:Option 𝓩yHu:Option 𝓩y5:Finset 𝓩y10:Finset 𝓩xHd:Option 𝓩1xHu:Option 𝓩1x5:Finset 𝓩1x10:Finset 𝓩1h2:yHd.toFinset βŠ† S5 ∧ yHu.toFinset βŠ† S5 ∧ y5 βŠ† S5 ∧ y10 βŠ† S10x:𝓩hx:x ∈ y10⊒ βˆƒ a ∈ y10, f a = f x All goals completed! πŸ™

B.2. Efficient definition for the cardinality of the preimage

The cardinality of the preimage of a charge Charges 𝓩1 in ofFinset S5 S10 βŠ† Charges 𝓩 under mapping charges through f : 𝓩 β†’+ 𝓩1.

def preimageOfFinsetCard (S5 S10 : Finset 𝓩) (f : 𝓩 β†’+ 𝓩1) (x : ChargeSpectrum 𝓩1) : β„• := let SHd := (S5.map ⟨Option.some, Option.some_injective π“©βŸ© βˆͺ {none} : Finset (Option 𝓩)).filter fun y => f <$> y = x.qHd let SHu := (S5.map ⟨Option.some, Option.some_injective π“©βŸ© βˆͺ {none} : Finset (Option 𝓩)).filter fun y => f <$> y = x.qHu let SQ5' := S5.filter fun y => f y ∈ x.Q5 let SQ5 : Finset (Finset 𝓩) := SQ5'.powerset.filter fun y => y.image f = x.Q5 let SQ10' := S10.filter fun y => f y ∈ x.Q10 let SQ10 : Finset (Finset 𝓩) := SQ10'.powerset.filter fun y => y.image f = x.Q10 SHd.card * SHu.card * SQ5.card * SQ10.card

B.3. Definition for the cardinality equals cardinality of the preimage

𝓩:Type𝓩1:Typeinst✝³:AddCommGroup 𝓩inst✝²:AddCommGroup 𝓩1inst✝¹:DecidableEq 𝓩1inst✝:DecidableEq 𝓩S5:Finset 𝓩S10:Finset 𝓩f:𝓩 β†’+ 𝓩1x:ChargeSpectrum 𝓩1⊒ preimageOfFinsetCard S5 S10 f x = {x_1 ∈ Finset.map { toFun := some, inj' := β‹― } S5 βˆͺ {none} | Option.map (⇑f) x_1 = x.qHd}.card * ({x_1 ∈ Finset.map { toFun := some, inj' := β‹― } S5 βˆͺ {none} | Option.map (⇑f) x_1 = x.qHu}.card * ({y ∈ {y ∈ S5 | f y ∈ x.Q5}.powerset | Finset.image (⇑f) y = x.Q5}.card * {y ∈ {y ∈ S10 | f y ∈ x.Q10}.powerset | Finset.image (⇑f) y = x.Q10}.card)) All goals completed! πŸ™