67 Definitions/MMFLM86NegPairingFockStep.lean:169:24: error: Type mismatch
Definitions/MMFLM86NegPairingFockStep.lean:169:24: error: Type mismatch
  hD i
has type
  (D i).osc = []
but is expected to have type
  l = []
Definitions/MMFLM86NegPairingFockStep.lean:175:2: error: Type mismatch
  Eq.symm
    (blockSum_subset bL form E a b j m (fun Q hQ => Finset.mem_biUnion.mpr (Exists.intro i ⟨Finset.mem_univ i, hQ⟩))
      fun Q x hQ => blockOfShift_eq_zero_of_not_mem_canonWindow bL form E a b j m (D i).a hQ)
has type
  (blockSum bL form E a b j m (canonWindow form a b j m (D i).a)) (iotaVL (D i).a) =
    (blockSum bL form E a b j m (Finset.univ.biUnion fun i => canonWindow form a b j m (D i).a)) (iotaVL (D i).a)
but is expected to have type
  ∑ Q ∈ canonWindow form a b j m (D i).a,
      honestBlockCoeffJ form a b j m Q • (blockOfShift bL form E a b j 0 m Q) (iotaVL (D i).a) =
---
73 Definitions/MMFLM86NegPairingFockStep.lean:175:2: error: Type mismatch
Definitions/MMFLM86NegPairingFockStep.lean:175:2: error: Type mismatch
  Eq.symm
    (blockSum_subset bL form E a b j m (fun Q hQ => Finset.mem_biUnion.mpr (Exists.intro i ⟨Finset.mem_univ i, hQ⟩))
      fun Q x hQ => blockOfShift_eq_zero_of_not_mem_canonWindow bL form E a b j m (D i).a hQ)
has type
  (blockSum bL form E a b j m (canonWindow form a b j m (D i).a)) (iotaVL (D i).a) =
    (blockSum bL form E a b j m (Finset.univ.biUnion fun i => canonWindow form a b j m (D i).a)) (iotaVL (D i).a)
but is expected to have type
  ∑ Q ∈ canonWindow form a b j m (D i).a,
      honestBlockCoeffJ form a b j m Q • (blockOfShift bL form E a b j 0 m Q) (iotaVL (D i).a) =
    (blockSum bL form E a b j m (Finset.univ.biUnion fun i => canonWindow form a b j m (D i).a)) (iotaVL (D i).a)
'MM.FLM86NPFS.FaceAtFamily' depends on axioms: [propext, Classical.choice, Quot.sound]
'MM.FLM86NPFS.honestNegPairingCoeffAtStates_iff_familyFaces' depends on axioms: [propext, Classical.choice, Quot.sound]
'MM.FLM86NPFS.FockStep' depends on axioms: [propext, Classical.choice, Quot.sound]
'MM.FLM86NPFS.fockStep_imp_oneMode' depends on axioms: [propext, Classical.choice, Quot.sound]
'MM.FLM86NPFS.faceAtFamily_lattice' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
---
93 --- FAILED: Definitions/MMFLM86NegPairingFockStep.lean ---
