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.FinCasesMapping 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 sectionA. 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)
symm π©: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
trans 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) (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 ext a π©: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
simp All goals completed! π
congr 1 e_f π©: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
funext a e_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
simp 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 := by π©:Typeπ©1:TypeinstβΒ²:AddCommGroup π©instβΒΉ:AddCommGroup π©1instβ:DecidableEq π©1f:π© β+ π©1x:ChargeSpectrum π©y:ChargeSpectrum π©h:x β yβ’ map f x β map f y
simp [map, subset_def] at * π©: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
obtain β¨hHd, hHu, hQ5, hQ10β© := h π©: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
refine β¨?_, ?_, ?_, ?_β© refine_1 π©: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).toFinsetrefine_2 π©: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).toFinsetrefine_3 π©: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.Q5refine_4 π©: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
Β· refine_1 π©: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
| β¨a, _, _, _β©, β¨b, _, _, _β© => π©: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
cases a none π©: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).toFinsetsome π©: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 cases b some.none π©: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).toFinsetsome.some π©: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 simp some.some π©: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 simp at hHd some.some π©: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β
subst hHd some.some π©: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β
rfl All goals completed! π
Β· refine_2 π©: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
| β¨_, a, _, _β©, β¨_, b, _, _β© => π©: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
cases a none π©: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).toFinsetsome π©: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 cases b some.none π©: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).toFinsetsome.some π©: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 simp some.some π©: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 simp at hHu some.some π©: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β
subst hHu some.some π©: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β
rfl All goals completed! π
Β· refine_3 π©: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 exact Finset.image_subset_image hQ5 All goals completed! π
Β· refine_4 π©: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 exact Finset.image_subset_image hQ10 All goals completed! πA.6. Mappings of charge spectra and charges of potential terms
lemma map_ofPotentialTerm_toFinset [DecidableEq π©]
(f : π© β+ π©1) (x : ChargeSpectrum π©) (T : PotentialTerm) :
(ofPotentialTerm (map f x) T).toFinset = (ofPotentialTerm x T).toFinset.image f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ ((map f x).ofPotentialTerm T).toFinset = Finset.image (βf) (x.ofPotentialTerm T).toFinset
have heq : β {W : Type} [AddCommGroup W] [DecidableEq W] (y : ChargeSpectrum W)
(S : PotentialTerm), (ofPotentialTerm y S).toFinset = (ofPotentialTerm' y S).toFinset := by
intro W _ _ y S π©:Typeπ©1:Typeinstββ΅:AddCommGroup π©instββ΄:AddCommGroup π©1instβΒ³:DecidableEq π©1instβΒ²:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermW:TypeinstβΒΉ:AddCommGroup Winstβ:DecidableEq Wy:ChargeSpectrum WS:PotentialTermβ’ (y.ofPotentialTerm S).toFinset = (y.ofPotentialTerm' S).toFinset π©: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
ext i π©:Typeπ©1:Typeinstββ΅:AddCommGroup π©instββ΄:AddCommGroup π©1instβΒ³:DecidableEq π©1instβΒ²:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermW:TypeinstβΒΉ:AddCommGroup Winstβ:DecidableEq Wy:ChargeSpectrum WS:PotentialTermi:Wβ’ i β (y.ofPotentialTerm S).toFinset β i β (y.ofPotentialTerm' S).toFinset π©: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
simp only [Multiset.mem_toFinset] π©:Typeπ©1:Typeinstββ΅:AddCommGroup π©instββ΄:AddCommGroup π©1instβΒ³:DecidableEq π©1instβΒ²:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermW:TypeinstβΒΉ:AddCommGroup Winstβ:DecidableEq Wy:ChargeSpectrum WS:PotentialTermi:Wβ’ i β y.ofPotentialTerm S β i β y.ofPotentialTerm' S π©: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
rw [mem_ofPotentialTerm_iff_mem_ofPotentialTerm π©:Typeπ©1:Typeinstββ΅:AddCommGroup π©instββ΄:AddCommGroup π©1instβΒ³:DecidableEq π©1instβΒ²:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermW:TypeinstβΒΉ:AddCommGroup Winstβ:DecidableEq Wy:ChargeSpectrum WS:PotentialTermi:Wβ’ i β y.ofPotentialTerm' S β i β y.ofPotentialTerm' S π©: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:π© β+ π©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:π© β+ π©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
rw [heq, π©: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:π© β+ π©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 heq π©: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:π© β+ π©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:π© β+ π©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
rcases x with β¨_ | qHd, _ | qHu, Q5, Q10β© none.none π©: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).toFinsetnone.some π©: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).toFinsetsome.none π©: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).toFinsetsome.some π©: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 <;> none.none π©: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).toFinsetnone.some π©: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).toFinsetsome.none π©: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).toFinsetsome.some π©: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 cases T some.some.ΞΌ π©: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.ΞΌ).toFinsetsome.some.Ξ² π©: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.Ξ²).toFinsetsome.some.Ξ π©: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.Ξ).toFinsetsome.some.W1 π©: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).toFinsetsome.some.W2 π©: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).toFinsetsome.some.W3 π©: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).toFinsetsome.some.W4 π©: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).toFinsetsome.some.K1 π©: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).toFinsetsome.some.K2 π©: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).toFinsetsome.some.topYukawa π©: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).toFinsetsome.some.bottomYukawa π©: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 <;> none.none.ΞΌ π©: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.ΞΌ).toFinsetnone.none.Ξ² π©: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.Ξ²).toFinsetnone.none.Ξ π©: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.Ξ).toFinsetnone.none.W1 π©: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).toFinsetnone.none.W2 π©: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).toFinsetnone.none.W3 π©: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).toFinsetnone.none.W4 π©: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).toFinsetnone.none.K1 π©: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).toFinsetnone.none.K2 π©: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).toFinsetnone.none.topYukawa π©: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).toFinsetnone.none.bottomYukawa π©: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).toFinsetnone.some.ΞΌ π©: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.ΞΌ).toFinsetnone.some.Ξ² π©: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.Ξ²).toFinsetnone.some.Ξ π©: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.Ξ).toFinsetnone.some.W1 π©: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).toFinsetnone.some.W2 π©: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).toFinsetnone.some.W3 π©: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).toFinsetnone.some.W4 π©: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).toFinsetnone.some.K1 π©: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).toFinsetnone.some.K2 π©: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).toFinsetnone.some.topYukawa π©: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).toFinsetnone.some.bottomYukawa π©: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).toFinsetsome.none.ΞΌ π©: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.ΞΌ).toFinsetsome.none.Ξ² π©: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.Ξ²).toFinsetsome.none.Ξ π©: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.Ξ).toFinsetsome.none.W1 π©: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).toFinsetsome.none.W2 π©: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).toFinsetsome.none.W3 π©: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).toFinsetsome.none.W4 π©: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).toFinsetsome.none.K1 π©: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).toFinsetsome.none.K2 π©: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).toFinsetsome.none.topYukawa π©: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).toFinsetsome.none.bottomYukawa π©: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).toFinsetsome.some.ΞΌ π©: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.ΞΌ).toFinsetsome.some.Ξ² π©: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.Ξ²).toFinsetsome.some.Ξ π©: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.Ξ).toFinsetsome.some.W1 π©: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).toFinsetsome.some.W2 π©: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).toFinsetsome.some.W3 π©: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).toFinsetsome.some.W4 π©: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).toFinsetsome.some.K1 π©: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).toFinsetsome.some.K2 π©: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).toFinsetsome.some.topYukawa π©: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).toFinsetsome.some.bottomYukawa π©: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
simp only [ofPotentialTerm', map, Option.map_eq_map, Option.map_some, Option.map_none,
Multiset.toFinset_map, Finset.val_toFinset, Function.comp_def, map_add, map_sub, map_neg,
Multiset.toFinset_singleton, Finset.image_singleton, Finset.product_eq_sprod,
β Finset.prodMap_image_product, Finset.image_image, Prod.map_fst, Prod.map_snd] All goals completed! π <;> none.none.ΞΌ π©: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 β
.toFinsetnone.none.Ξ² π©: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 β
.toFinsetnone.none.W2 π©: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 β
.toFinsetnone.none.W3 π©: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 β
.toFinsetnone.none.W4 π©: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 β
.toFinsetnone.none.K2 π©: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 β
.toFinsetnone.none.topYukawa π©: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 β
.toFinsetnone.none.bottomYukawa π©: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 β
.toFinsetnone.some.ΞΌ π©: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 β
.toFinsetnone.some.W2 π©: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 β
.toFinsetnone.some.W4 π©: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 β
.toFinsetnone.some.K2 π©: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 β
.toFinsetnone.some.bottomYukawa π©: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 β
.toFinsetsome.none.ΞΌ π©: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 β
.toFinsetsome.none.Ξ² π©: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 β
.toFinsetsome.none.W3 π©: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 β
.toFinsetsome.none.W4 π©: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 β
.toFinsetsome.none.K2 π©: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 β
.toFinsetsome.none.topYukawa π©: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
simp All goals completed! π
lemma mem_map_ofPotentialTerm_iff [DecidableEq π©]
(f : π© β+ π©1) (x : ChargeSpectrum π©) (T : PotentialTerm) :
i β (ofPotentialTerm (map f x) T) β i β (ofPotentialTerm x T).map f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β (map f x).ofPotentialTerm T β i β Multiset.map (βf) (x.ofPotentialTerm T)
trans i β (ofPotentialTerm (map f x) T).toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β (map f x).ofPotentialTerm T β i β ((map f x).ofPotentialTerm T).toFinsetπ©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β ((map f x).ofPotentialTerm T).toFinset β i β Multiset.map (βf) (x.ofPotentialTerm T)
Β· π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β (map f x).ofPotentialTerm T β i β ((map f x).ofPotentialTerm T).toFinset simp All goals completed! π
rw [map_ofPotentialTerm_toFinset π©: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) π©: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)] π©: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)
simp All goals completed! π
lemma mem_map_ofPotentialTerm'_iff[DecidableEq π©]
(f : π© β+ π©1) (x : ChargeSpectrum π©) (T : PotentialTerm) :
i β (ofPotentialTerm' (map f x) T) β i β (ofPotentialTerm' x T).map f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β (map f x).ofPotentialTerm' T β i β Multiset.map (βf) (x.ofPotentialTerm' T)
rw [β mem_ofPotentialTerm_iff_mem_ofPotentialTerm π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1i:π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ i β (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β’ i β (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β’ i β (map f x).ofPotentialTerm T β i β Multiset.map (βf) (x.ofPotentialTerm' T)
rw [mem_map_ofPotentialTerm_iff π©: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β’ 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β’ i β Multiset.map (βf) (x.ofPotentialTerm T) β i β Multiset.map (βf) (x.ofPotentialTerm' T)
simp only [Multiset.mem_map] π©: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
constructor mp π©: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 = impr π©: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
Β· mp π©: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 intro β¨a, h, h1β© mp π©: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
refine β¨a, ?_, h1β© mp π©: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
exact mem_ofPotentialTerm_iff_mem_ofPotentialTerm.mp h All goals completed! π
Β· mpr π©: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 intro β¨a, h, h1β© mpr π©: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
refine β¨a, ?_, h1β© mpr π©: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
exact mem_ofPotentialTerm_iff_mem_ofPotentialTerm.mpr h All goals completed! π
lemma map_ofPotentialTerm'_toFinset [DecidableEq π©]
(f : π© β+ π©1) (x : ChargeSpectrum π©) (T : PotentialTerm) :
(ofPotentialTerm' (map f x) T).toFinset = (ofPotentialTerm' x T).toFinset.image f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermβ’ ((map f x).ofPotentialTerm' T).toFinset = Finset.image (βf) (x.ofPotentialTerm' T).toFinset
ext i π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermi:π©1β’ i β ((map f x).ofPotentialTerm' T).toFinset β i β Finset.image (βf) (x.ofPotentialTerm' T).toFinset
simp only [Multiset.mem_toFinset, Finset.mem_image] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermi:π©1β’ i β (map f x).ofPotentialTerm' T β β a β x.ofPotentialTerm' T, f a = i
rw [mem_map_ofPotentialTerm'_iff π©: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 π©: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] π©: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
simp 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 := by π©: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
cases 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.ΞW1 π©: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.W1W2 π©: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.W2W3 π©: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.W3W4 π©: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.W4K1 π©: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.K1K2 π©: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.K2topYukawa π©: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.topYukawabottomYukawa π©: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 simp [allowsTermForm, map] All goals completed! πA.8. Mapping preserves whether a charge spectrum allows a potential term
lemma map_allowsTerm {f : π© β+ π©1} {x : ChargeSpectrum π©} {T : PotentialTerm}
(h : x.AllowsTerm T) : (map f x).AllowsTerm T := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermh:x.AllowsTerm Tβ’ (map f x).AllowsTerm T
rw [allowsTerm_iff_subset_allowsTermForm π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermh:β a b c, allowsTermForm a b c T β xβ’ β a b c, allowsTermForm a b c T β map f x π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermh:β a b c, allowsTermForm a b c T β xβ’ β a b c, allowsTermForm a b c T β map f x] at β’ h π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTermh:β a b c, allowsTermForm a b c T β xβ’ β a b c, allowsTermForm a b c T β map f x
obtain β¨a, b, c, h1β© := h π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTerma:π©b:π©c:π©h1:allowsTermForm a b c T β xβ’ β a b c, allowsTermForm a b c T β map f x
use f a, f b, f c h π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©T:PotentialTerma:π©b:π©c:π©h1:allowsTermForm a b c T β xβ’ allowsTermForm (f a) (f b) (f c) T β map f x
rw [β allowsTermForm_map h π©: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 h π©: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]h π©: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
exact map_subset h1 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 := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©h:x.IsPhenoConstrainedβ’ (map f x).IsPhenoConstrained
simp [IsPhenoConstrained] at β’ h π©: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
rcases h with h | h | h | h | h | h | h | h inl π©: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.W1inr.inl π©: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.W1inr.inr.inl π©: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.W1inr.inr.inr.inl π©: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.W1inr.inr.inr.inr.inl π©: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.W1inr.inr.inr.inr.inr.inl π©: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.W1inr.inr.inr.inr.inr.inr.inl π©: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.W1inr.inr.inr.inr.inr.inr.inr π©: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
Β· inl π©: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 exact Or.inl (map_allowsTerm h) All goals completed! π
Β· inr.inl π©: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 exact Or.inr (Or.inl (map_allowsTerm h)) All goals completed! π
Β· inr.inr.inl π©: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 exact Or.inr (Or.inr (Or.inl (map_allowsTerm h))) All goals completed! π
Β· inr.inr.inr.inl π©: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 exact Or.inr (Or.inr (Or.inr (Or.inl (map_allowsTerm h)))) All goals completed! π
Β· inr.inr.inr.inr.inl π©: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 exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (map_allowsTerm h))))) All goals completed! π
Β· inr.inr.inr.inr.inr.inl π©: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 exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (map_allowsTerm h)))))) All goals completed! π
Β· inr.inr.inr.inr.inr.inr.inl π©: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 exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (map_allowsTerm h))))))) All goals completed! π
Β· inr.inr.inr.inr.inr.inr.inr π©: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 exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ((map_allowsTerm h)))))))) 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 := by π©:Typeπ©1:TypeinstβΒ²:AddCommGroup π©instβΒΉ:AddCommGroup π©1instβ:DecidableEq π©1f:π© β+ π©1x:ChargeSpectrum π©β’ (map f x).IsComplete β x.IsComplete
simp [IsComplete, map] All goals completed! πA.11. Mapping commutes with charges of Yukawa terms
lemma map_ofYukawaTerms_toFinset {f : π© β+ π©1} {x : ChargeSpectrum π©} :
(map f x).ofYukawaTerms.toFinset = x.ofYukawaTerms.toFinset.image f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©β’ (map f x).ofYukawaTerms.toFinset = Finset.image (βf) x.ofYukawaTerms.toFinset
simp [ofYukawaTerms] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©β’ ((map f x).ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
((map f x).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset =
Finset.image (βf)
((x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset)
ext i π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β
((map f x).ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
((map f x).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset β
i β
Finset.image (βf)
((x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset)
rw [Finset.image_union π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β
((map f x).ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
((map f x).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset β
i β
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β
((map f x).ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
((map f x).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset β
i β
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β
((map f x).ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
((map f x).ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset β
i β
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset βͺ
Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset
simp only [Finset.mem_union, Multiset.mem_toFinset] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β (map f x).ofPotentialTerm' PotentialTerm.topYukawa β¨ i β (map f x).ofPotentialTerm' PotentialTerm.bottomYukawa β
i β Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset β¨
i β Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset
rw [mem_map_ofPotentialTerm'_iff, π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β Multiset.map (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa) β¨
i β (map f x).ofPotentialTerm' PotentialTerm.bottomYukawa β
i β Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.topYukawa).toFinset β¨
i β Finset.image (βf) (x.ofPotentialTerm' PotentialTerm.bottomYukawa).toFinset π©: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 mem_map_ofPotentialTerm'_iff π©: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 π©: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] π©: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
simp [Multiset.mem_map] All goals completed! π
lemma mem_map_ofYukawaTerms_iff {f : π© β+ π©1} {x : ChargeSpectrum π©} {i} :
i β (map f x).ofYukawaTerms β i β x.ofYukawaTerms.map f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β (map f x).ofYukawaTerms β i β Multiset.map (βf) x.ofYukawaTerms
trans i β (map f x).ofYukawaTerms.toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β (map f x).ofYukawaTerms β i β (map f x).ofYukawaTerms.toFinsetπ©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β (map f x).ofYukawaTerms.toFinset β i β Multiset.map (βf) x.ofYukawaTerms
Β· π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©i:π©1β’ i β (map f x).ofYukawaTerms β i β (map f x).ofYukawaTerms.toFinset simp All goals completed! π
rw [map_ofYukawaTerms_toFinset π©: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 π©: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] π©: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
simp All goals completed! πA.12. Mapping of charge spectra and regenerating dangerous Yukawa terms
lemma map_ofYukawaTermsNSum_toFinset {f : π© β+ π©1} {x : ChargeSpectrum π©} {n : β}:
((map f x).ofYukawaTermsNSum n).toFinset = (x.ofYukawaTermsNSum n).toFinset.image f:= by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:ββ’ ((map f x).ofYukawaTermsNSum n).toFinset = Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset
induction n with
| zero => zero π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©β’ ((map f x).ofYukawaTermsNSum 0).toFinset = Finset.image (βf) (x.ofYukawaTermsNSum 0).toFinset simp [ofYukawaTermsNSum] All goals completed! π
| succ n ih => succ π©: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).toFinsetβ’ ((map f x).ofYukawaTermsNSum (n + 1)).toFinset = Finset.image (βf) (x.ofYukawaTermsNSum (n + 1)).toFinset
simp [ofYukawaTermsNSum] succ π©: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).toFinsetβ’ ((map f x).ofYukawaTermsNSum n).toFinset βͺ
(((map f x).ofYukawaTermsNSum n).bind fun sSum =>
Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset =
Finset.image (βf)
((x.ofYukawaTermsNSum n).toFinset βͺ
((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset)
rw [Finset.image_union succ π©: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).toFinsetβ’ ((map f x).ofYukawaTermsNSum n).toFinset βͺ
(((map f x).ofYukawaTermsNSum n).bind fun sSum =>
Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset =
Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset βͺ
Finset.image (βf)
((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset succ π©: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).toFinsetβ’ ((map f x).ofYukawaTermsNSum n).toFinset βͺ
(((map f x).ofYukawaTermsNSum n).bind fun sSum =>
Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset =
Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset βͺ
Finset.image (βf)
((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset] succ π©: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).toFinsetβ’ ((map f x).ofYukawaTermsNSum n).toFinset βͺ
(((map f x).ofYukawaTermsNSum n).bind fun sSum =>
Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset =
Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset βͺ
Finset.image (βf)
((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset
congr 1 e_a π©: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).toFinsetβ’ (((map f x).ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset =
Finset.image (βf) ((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset
ext i e_a π©: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:π©1β’ i β
(((map f x).ofYukawaTermsNSum n).bind fun sSum =>
Multiset.map (fun s => sSum + s) (map f x).ofYukawaTerms).toFinset β
i β
Finset.image (βf)
((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset
simp only [Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map, Finset.mem_image,
exists_exists_and_exists_and_eq_and, map_add] e_a π©: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:π©1β’ (β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i) β
β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
constructor e_a.mp π©: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:π©1β’ (β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i) β
β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = ie_a.mpr π©: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:π©1β’ (β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i) β
β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i
Β· e_a.mp π©: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:π©1β’ (β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i) β
β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i intro h e_a.mp π©: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:π©1h:β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = iβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
obtain β¨a, a_mem, b, b_mem, hβ© := h e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = iβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
have a_mem' : a β ((map f x).ofYukawaTermsNSum n).toFinset := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:ββ’ ((map f x).ofYukawaTermsNSum n).toFinset = Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β ((map f x).ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i simpa using a_meme_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β ((map f x).ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = ie_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β ((map f x).ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
rw [ih e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i] at a_mem'e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β (map f x).ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
rw [mem_map_ofYukawaTerms_iff e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β Multiset.map (βf) x.ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β Multiset.map (βf) x.ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i] at b_meme_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1b_mem:b β Multiset.map (βf) x.ofYukawaTermsh:a + b = ia_mem':a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinsetβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
simp at a_mem' b_mem e_a.mp π©: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:π©1a_mem:a β (map f x).ofYukawaTermsNSum nb:π©1h:a + b = ia_mem':β a_1 β x.ofYukawaTermsNSum n, f a_1 = ab_mem:β a β x.ofYukawaTerms, f a = bβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
obtain β¨a, a_mem', rflβ© := a_mem' e_a.mp π©: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:π©1b:π©1b_mem:β a β x.ofYukawaTerms, f a = ba:π©a_mem':a β x.ofYukawaTermsNSum na_mem:f a β (map f x).ofYukawaTermsNSum nh:f a + b = iβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
obtain β¨b, b_mem', rflβ© := b_mem e_a.mp π©: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 na_mem:f a β (map f x).ofYukawaTermsNSum nb:π©b_mem':b β x.ofYukawaTermsh:f a + f b = iβ’ β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i
exact β¨a, a_mem', b, b_mem', hβ© All goals completed! π
Β· e_a.mpr π©: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:π©1β’ (β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = i) β
β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i intro h e_a.mpr π©: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:π©1h:β a β x.ofYukawaTermsNSum n, β b β x.ofYukawaTerms, f a + f b = iβ’ β a β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i
obtain β¨a, a_mem, b, b_mem, hβ© := h e_a.mpr π©: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 β (map f x).ofYukawaTermsNSum n, β a_1 β (map f x).ofYukawaTerms, a + a_1 = i
use f a h π©: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 a β (map f x).ofYukawaTermsNSum n β§ β a_1 β (map f x).ofYukawaTerms, f a + a_1 = i
apply And.intro h.left π©: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 a β (map f x).ofYukawaTermsNSum nh.right π©: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_1 β (map f x).ofYukawaTerms, f a + a_1 = i
Β· h.left π©: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 a β (map f x).ofYukawaTermsNSum n rw [β Multiset.mem_toFinset, h.left π©: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 a β ((map f x).ofYukawaTermsNSum n).toFinset h.left π©: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 a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset ih h.left π©: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 a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinseth.left π©: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 a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset]h.left π©: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 a β Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset
simp only [Finset.mem_image, Multiset.mem_toFinset] h.left π©: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_1 β x.ofYukawaTermsNSum n, f a_1 = f a
use a All goals completed! π
use f b h π©: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 β (map f x).ofYukawaTerms β§ f a + f b = i
apply And.intro h.left π©: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 β (map f x).ofYukawaTermsh.right π©: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 a + f b = i
Β· h.left π©: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 β (map f x).ofYukawaTerms rw [mem_map_ofYukawaTerms_iff h.left π©: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 h.left π©: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]h.left π©: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
simp only [Multiset.mem_map] h.left π©: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
use b All goals completed! π
exact h All goals completed! π
lemma mem_map_ofYukawaTermsNSum_iff {f : π© β+ π©1} {x : ChargeSpectrum π©} {n i} :
i β (map f x).ofYukawaTermsNSum n β i β (x.ofYukawaTermsNSum n).map f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βi:π©1β’ i β (map f x).ofYukawaTermsNSum n β i β Multiset.map (βf) (x.ofYukawaTermsNSum n)
trans i β ((map f x).ofYukawaTermsNSum n).toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βi:π©1β’ i β (map f x).ofYukawaTermsNSum n β i β ((map f x).ofYukawaTermsNSum n).toFinsetπ©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βi:π©1β’ i β ((map f x).ofYukawaTermsNSum n).toFinset β i β Multiset.map (βf) (x.ofYukawaTermsNSum n)
Β· π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βi:π©1β’ i β (map f x).ofYukawaTermsNSum n β i β ((map f x).ofYukawaTermsNSum n).toFinset simp All goals completed! π
rw [map_ofYukawaTermsNSum_toFinset π©: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) π©: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)] π©: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)
simp All goals completed! πlemma map_phenoConstrainingChargesSP_toFinset {f : π© β+ π©1} {x : ChargeSpectrum π©} :
(map f x).phenoConstrainingChargesSP.toFinset =
x.phenoConstrainingChargesSP.toFinset.image f := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©β’ (map f x).phenoConstrainingChargesSP.toFinset = Finset.image (βf) x.phenoConstrainingChargesSP.toFinset
simp [phenoConstrainingChargesSP, map_ofPotentialTerm'_toFinset, Finset.image_union] All goals completed! π
lemma map_yukawaGeneratesDangerousAtLevel (f : π© β+ π©1) {x : ChargeSpectrum π©} (n : β)
(h : x.YukawaGeneratesDangerousAtLevel n) : (map f x).YukawaGeneratesDangerousAtLevel n := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ (map f x).YukawaGeneratesDangerousAtLevel n
rw [yukawaGeneratesDangerousAtLevel_iff_toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ ((map f x).ofYukawaTermsNSum n).toFinset β© (map f x).phenoConstrainingChargesSP.toFinset β β
π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ ((map f x).ofYukawaTermsNSum n).toFinset β© (map f x).phenoConstrainingChargesSP.toFinset β β
] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ ((map f x).ofYukawaTermsNSum n).toFinset β© (map f x).phenoConstrainingChargesSP.toFinset β β
rw [map_phenoConstrainingChargesSP_toFinset, π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ ((map f x).ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset β β
π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset β β
map_ofYukawaTermsNSum_toFinset π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset β β
π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset β β
] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset β β
rw [β Finset.nonempty_iff_ne_empty, π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ (Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset β© Finset.image (βf) x.phenoConstrainingChargesSP.toFinset).Nonempty π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Β¬Disjoint (Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset) (Finset.image (βf) x.phenoConstrainingChargesSP.toFinset) β Finset.not_disjoint_iff_nonempty_inter π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Β¬Disjoint (Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset) (Finset.image (βf) x.phenoConstrainingChargesSP.toFinset) π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Β¬Disjoint (Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset) (Finset.image (βf) x.phenoConstrainingChargesSP.toFinset)] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Β¬Disjoint (Finset.image (βf) (x.ofYukawaTermsNSum n).toFinset) (Finset.image (βf) x.phenoConstrainingChargesSP.toFinset)
apply Disjoint.of_image_finset.mt π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©f:π© β+ π©1x:ChargeSpectrum π©n:βh:x.YukawaGeneratesDangerousAtLevel nβ’ Β¬Disjoint (x.ofYukawaTermsNSum n).toFinset x.phenoConstrainingChargesSP.toFinset
rw [Finset.not_disjoint_iff_nonempty_inter, π©: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).Nonempty π©: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 β β
Finset.nonempty_iff_ne_empty π©: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 β β
π©: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 β β
] π©: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 β β
exact (yukawaGeneratesDangerousAtLevel_iff_toFinset _ _).mp h 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
lemma preimageOfFinset_eq (S5 S10 : Finset π©) (f : π© β+ π©1) (x : ChargeSpectrum π©1) :
preimageOfFinset S5 S10 f x = {y : ChargeSpectrum π© | y.map f = x β§ y β ofFinset S5 S10} := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ β(preimageOfFinset S5 S10 f x) = {y | map f y = x β§ y β ofFinset S5 S10}
ext y π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1y:ChargeSpectrum π©β’ y β β(preimageOfFinset S5 S10 f x) β y β {y | map f y = x β§ y β ofFinset S5 S10}
simp [preimageOfFinset, toProd] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1y:ChargeSpectrum π©β’ (β a a_1 a_2 b,
(((a = none β¨ β a_3 β S5, some a_3 = a) β§ Option.map (βf) a = x.qHd) β§
((a_1 = none β¨ β a β S5, some a = a_1) β§ Option.map (βf) a_1 = x.qHu) β§
(a_2 β {y β S5 | f y β x.Q5} β§ Finset.image (βf) a_2 = x.Q5) β§
b β {y β S10 | f y β x.Q10} β§ Finset.image (βf) b = x.Q10) β§
{ qHd := a, qHu := a_1, Q5 := a_2, Q10 := b } = y) β
map f y = x β§ y β ofFinset S5 S10
match y, x with
| β¨yHd, yHu, y5, y10β©, β¨xHd, xHu, x5, x10β© => π©: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 π©1β’ (β a a_1 a_2 b,
(((a = none β¨ β a_3 β S5, some a_3 = a) β§
Option.map (βf) a = { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.qHd) β§
((a_1 = none β¨ β a β S5, some a = a_1) β§
Option.map (βf) a_1 = { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.qHu) β§
(a_2 β {y β S5 | f y β { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.Q5} β§
Finset.image (βf) a_2 = { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.Q5) β§
b β {y β S10 | f y β { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.Q10} β§
Finset.image (βf) b = { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 }.Q10) β§
{ qHd := a, qHu := a_1, Q5 := a_2, Q10 := b } = { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 }) β
map f { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } = { qHd := xHd, qHu := xHu, Q5 := x5, Q10 := x10 } β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10
simp [map] π©: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 π©1β’ ((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = xHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = xHu) β§
(y5 β {x β S5 | f x β x5} β§ Finset.image (βf) y5 = x5) β§
y10 β {x β S10 | f x β x10} β§ Finset.image (βf) y10 = x10 β
(Option.map (βf) yHd = xHd β§ Option.map (βf) yHu = xHu β§ Finset.image (βf) y5 = x5 β§ Finset.image (βf) y10 = x10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10
constructor mp π©: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 π©1β’ ((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = xHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = xHu) β§
(y5 β {x β S5 | f x β x5} β§ Finset.image (βf) y5 = x5) β§
y10 β {x β S10 | f x β x10} β§ Finset.image (βf) y10 = x10 β
(Option.map (βf) yHd = xHd β§ Option.map (βf) yHu = xHu β§ Finset.image (βf) y5 = x5 β§ Finset.image (βf) y10 = x10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10mpr π©: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 π©1β’ (Option.map (βf) yHd = xHd β§ Option.map (βf) yHu = xHu β§ Finset.image (βf) y5 = x5 β§ Finset.image (βf) y10 = x10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10 β
((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = xHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = xHu) β§
(y5 β {x β S5 | f x β x5} β§ Finset.image (βf) y5 = x5) β§ y10 β {x β S10 | f x β x10} β§ Finset.image (βf) y10 = x10
Β· mp π©: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 π©1β’ ((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = xHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = xHu) β§
(y5 β {x β S5 | f x β x5} β§ Finset.image (βf) y5 = x5) β§
y10 β {x β S10 | f x β x10} β§ Finset.image (βf) y10 = x10 β
(Option.map (βf) yHd = xHd β§ Option.map (βf) yHu = xHu β§ Finset.image (βf) y5 = x5 β§ Finset.image (βf) y10 = x10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10 intro β¨β¨h1, rflβ©, β¨h2, rflβ©, β¨h3, rflβ©, β¨h4, rflβ©β© mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ (Option.map (βf) yHd = Option.map (βf) yHd β§
Option.map (βf) yHu = Option.map (βf) yHu β§
Finset.image (βf) y5 = Finset.image (βf) y5 β§ Finset.image (βf) y10 = Finset.image (βf) y10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10
simp only [true_and] mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ { qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10
rw [mem_ofFinset_iff mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ { 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 mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ { 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] mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ { 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
simp only mp π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ yHd.toFinset β S5 β§ yHu.toFinset β S5 β§ y5 β S5 β§ y10 β S10
refine β¨?_, ?_, ?_, ?_β© mp.refine_1 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ yHd.toFinset β S5mp.refine_2 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ yHu.toFinset β S5mp.refine_3 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ y5 β S5mp.refine_4 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ y10 β S10
Β· mp.refine_1 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ yHd.toFinset β S5 match yHd with
| 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 π©1h2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}a:π©h1:some a = none β¨ β a_1 β S5, some a_1 = some aβ’ (some a).toFinset β S5 simpa using h1 All goals completed! π
| none => π©: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:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}h1:none = none β¨ β a β S5, some a = noneβ’ none.toFinset β S5 simp All goals completed! π
Β· mp.refine_2 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ yHu.toFinset β S5 match yHu with
| 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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}a:π©h2:some a = none β¨ β a_1 β S5, some a_1 = some aβ’ (some a).toFinset β S5 simpa using h2 All goals completed! π
| none => π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}h2:none = none β¨ β a β S5, some a = noneβ’ none.toFinset β S5 simp All goals completed! π
Β· mp.refine_3 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ y5 β S5 exact h3.trans <| Finset.filter_subset (fun y => f y β Finset.image (βf) y5) S5 All goals completed! π
Β· mp.refine_4 π©: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 π©1h1:yHd = none β¨ β a β S5, some a = yHdh2:yHu = none β¨ β a β S5, some a = yHuh3:y5 β {x β S5 | f x β Finset.image (βf) y5}h4:y10 β {x β S10 | f x β Finset.image (βf) y10}β’ y10 β S10 apply h4.trans <| Finset.filter_subset (fun y => f y β Finset.image (βf) y10) S10 All goals completed! π
Β· mpr π©: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 π©1β’ (Option.map (βf) yHd = xHd β§ Option.map (βf) yHu = xHu β§ Finset.image (βf) y5 = x5 β§ Finset.image (βf) y10 = x10) β§
{ qHd := yHd, qHu := yHu, Q5 := y5, Q10 := y10 } β ofFinset S5 S10 β
((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = xHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = xHu) β§
(y5 β {x β S5 | f x β x5} β§ Finset.image (βf) y5 = x5) β§ y10 β {x β S10 | f x β x10} β§ Finset.image (βf) y10 = x10 intro β¨β¨rfl, rfl, rfl, rflβ©, h2β© mpr π©: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 } β ofFinset S5 S10β’ ((yHd = none β¨ β a β S5, some a = yHd) β§ Option.map (βf) yHd = Option.map (βf) yHd) β§
((yHu = none β¨ β a β S5, some a = yHu) β§ Option.map (βf) yHu = Option.map (βf) yHu) β§
(y5 β {x β S5 | f x β Finset.image (βf) y5} β§ Finset.image (βf) y5 = Finset.image (βf) y5) β§
y10 β {x β S10 | f x β Finset.image (βf) y10} β§ Finset.image (βf) y10 = Finset.image (βf) y10
simp only [and_true, Finset.mem_image] mpr π©: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 } β ofFinset S5 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}
rw [mem_ofFinset_iff mpr π©: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} mpr π©: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}] at h2mpr π©: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}
simp at h2 mpr π©: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}
refine β¨?_, ?_, ?_, ?_β© mpr.refine_1 π©: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 = yHdmpr.refine_2 π©: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 = yHumpr.refine_3 π©: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}mpr.refine_4 π©: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}
Β· mpr.refine_1 π©: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
| 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:(some a).toFinset β S5 β§ yHu.toFinset β S5 β§ y5 β S5 β§ y10 β S10β’ some a = none β¨ β a_1 β S5, some a_1 = some a
simp at h2 π©: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
simpa using h2.1 All goals completed! π
| none => π©: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 simp All goals completed! π
Β· mpr.refine_2 π©: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
| 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 β§ (some a).toFinset β S5 β§ y5 β S5 β§ y10 β S10β’ some a = none β¨ β a_1 β S5, some a_1 = some a
simp at h2 π©: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
simpa using h2.2.1 All goals completed! π
| none => π©: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 simp All goals completed! π
Β· mpr.refine_3 π©: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} refine Finset.subset_iff.mpr ?_ mpr.refine_3 π©: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}
intro x hx mpr.refine_3 π©: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}
simp only [Finset.mem_filter] mpr.refine_3 π©: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
refine β¨h2.2.2.1 hx, ?_β© mpr.refine_3 π©: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
use x All goals completed! π
Β· mpr.refine_4 π©: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} refine Finset.subset_iff.mpr ?_ mpr.refine_4 π©: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}
intro x hx mpr.refine_4 π©: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}
simp only [Finset.mem_filter] mpr.refine_4 π©: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
refine β¨h2.2.2.2 hx, ?_β© mpr.refine_4 π©: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
use 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.cardB.3. Definition for the cardinality equals cardinality of the preimage
lemma preimageOfFinset_card_eq (S5 S10 : Finset π©) (f : π© β+ π©1) (x : ChargeSpectrum π©1) :
preimageOfFinsetCard S5 S10 f x =
(preimageOfFinset S5 S10 f x).card := by π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x = (preimageOfFinset S5 S10 f x).card
rw [preimageOfFinset, π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x =
(Finset.map toProd.symm.toEmbedding
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHd}.product
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHu}.product
({y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5}.product
({y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10}))))).card π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x =
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHd}.product
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHu}.product
({y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5}.product
({y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10})))).card Finset.card_map π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x =
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHd}.product
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHu}.product
({y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5}.product
({y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10})))).card π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x =
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHd}.product
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHu}.product
({y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5}.product
({y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10})))).card] π©:Typeπ©1:TypeinstβΒ³:AddCommGroup π©instβΒ²:AddCommGroup π©1instβΒΉ:DecidableEq π©1instβ:DecidableEq π©S5:Finset π©S10:Finset π©f:π© β+ π©1x:ChargeSpectrum π©1β’ preimageOfFinsetCard S5 S10 f x =
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHd}.product
({y β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | βf <$> y = x.qHu}.product
({y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5}.product
({y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10})))).card
simp only [Option.map_eq_map, Finset.product_eq_sprod] π©: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} ΓΛ’
{x_1 β Finset.map { toFun := some, inj' := β― } S5 βͺ {none} | Option.map (βf) x_1 = x.qHu} ΓΛ’
{y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5} ΓΛ’
{y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10}).card
repeat rw [Finset.card_product π©: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} ΓΛ’
{y β {y β S5 | f y β x.Q5}.powerset | Finset.image (βf) y = x.Q5} ΓΛ’
{y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10}).card π©: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))] π©: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} ΓΛ’
{y β {y β S10 | f y β x.Q10}.powerset | Finset.image (βf) y = x.Q10}).card) π©: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)) π©: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))
simp [preimageOfFinsetCard, mul_assoc] All goals completed! π