67 Definitions/MMFLM86NegPairingFockStep.lean:118:10: error(lean.unknownIdentifier): Unknown identifier `blockOfShift`
Definitions/MMFLM86NegPairingFockStep.lean:118:10: error(lean.unknownIdentifier): Unknown identifier `blockOfShift`
Definitions/MMFLM86NegPairingFockStep.lean:126:2: error: Type mismatch
  Iff.rfl
has type
  ?m.51 ↔ ?m.51
but is expected to have type
  HonestNegPairingCoeffAtStates bL form E ↔
    ∀ (a b : L),
      (form a) b < 0 → ∀ (j : ℕ) (m : ℤ) (n : ℕ) (D : Fin n → StateDatum L), FaceAtFamily bL form E a b j m n D
Definitions/MMFLM86NegPairingFockStep.lean:163:60: error: Invalid argument name `F` for function `canonWindow`

Hint: Perhaps you meant one of the following parameter names:
  • `L`: F̵L̲
  • `form`: F̵f̲o̲r̲m̲
---
68 Definitions/MMFLM86NegPairingFockStep.lean:126:2: error: Type mismatch
Definitions/MMFLM86NegPairingFockStep.lean:126:2: error: Type mismatch
  Iff.rfl
has type
  ?m.51 ↔ ?m.51
but is expected to have type
  HonestNegPairingCoeffAtStates bL form E ↔
    ∀ (a b : L),
      (form a) b < 0 → ∀ (j : ℕ) (m : ℤ) (n : ℕ) (D : Fin n → StateDatum L), FaceAtFamily bL form E a b j m n D
Definitions/MMFLM86NegPairingFockStep.lean:163:60: error: Invalid argument name `F` for function `canonWindow`

Hint: Perhaps you meant one of the following parameter names:
  • `L`: F̵L̲
  • `form`: F̵f̲o̲r̲m̲
  • `a`: F̵a̲
---
76 Definitions/MMFLM86NegPairingFockStep.lean:163:60: error: Invalid argument name `F` for function `canonWindow`
Definitions/MMFLM86NegPairingFockStep.lean:163:60: error: Invalid argument name `F` for function `canonWindow`

Hint: Perhaps you meant one of the following parameter names:
  • `L`: F̵L̲
  • `form`: F̵f̲o̲r̲m̲
  • `a`: F̵a̲
  • `b`: F̵b̲
  • `j`: F̵j̲
  • `m`: F̵m̲
  • `c`: F̵c̲
Definitions/MMFLM86NegPairingFockStep.lean:166:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (D i).osc
in the target expression
  stateOfVL bL form (D i) = iotaVL (D i).a
---
86 Definitions/MMFLM86NegPairingFockStep.lean:166:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
Definitions/MMFLM86NegPairingFockStep.lean:166:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (D i).osc
in the target expression
  stateOfVL bL form (D i) = iotaVL (D i).a

F : Type u
inst✝⁵ : Field F
inst✝⁴ : CharZero F
L : Type v
inst✝³ : AddCommGroup L
inst✝² : Module.Free ℤ L
κ : Type w
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
---
113 Definitions/MMFLM86NegPairingFockStep.lean:191:4: error: Type mismatch
Definitions/MMFLM86NegPairingFockStep.lean:191:4: error: Type mismatch
  h a b hab j m n fun i => { osc := T i ++ (D i).osc, a := (D i).a }
has type
  ∃ s,
    ∀ (i : Fin n),
      ((ZAligned bL form E) ((YFam bL form E a (-↑j - 1)) ((creationExpVL bL form b 0) (iotaVL b))) m)
          (stateOfVL bL form { osc := T i ++ (D i).osc, a := (D i).a }) =
        ∑ Q ∈ s,
          honestBlockCoeffJ form a b j m Q •
            (FLM86NPNA.blockOfShift bL form E a b j 0 m Q) (stateOfVL bL form { osc := T i ++ (D i).osc, a := (D i).a })
but is expected to have type
  FaceAtFamily bL form E a b j m n fun i => { osc := T i ++ (D i).osc, a := (D i).a }
Definitions/MMFLM86NegPairingFockStep.lean:203:36: error(lean.unknownIdentifier): Unknown identifier `not_eq_iff`
Definitions/MMFLM86NegPairingFockStep.lean:222:4: error: Type mismatch
---
125 Definitions/MMFLM86NegPairingFockStep.lean:203:36: error(lean.unknownIdentifier): Unknown identifier `not_eq_iff`
Definitions/MMFLM86NegPairingFockStep.lean:203:36: error(lean.unknownIdentifier): Unknown identifier `not_eq_iff`
Definitions/MMFLM86NegPairingFockStep.lean:222:4: error: Type mismatch
  key (∑ i, (D i).osc.length) n D rfl
has type
  FaceAtFamily bL form E a b j m n D
but is expected to have type
  ∃ s,
    ∀ (i : Fin n),
      ((ZAligned bL form E) ((YFam bL form E a (-↑j - 1)) ((creationExpVL bL form b 0) (iotaVL b))) m)
          (stateOfVL bL form (D i)) =
        ∑ Q ∈ s,
          honestBlockCoeffJ form a b j m Q • (FLM86NPNA.blockOfShift bL form E a b j 0 m Q) (stateOfVL bL form (D i))
'MM.FLM86NPFS.FaceAtFamily' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
'MM.FLM86NPFS.honestNegPairingCoeffAtStates_iff_familyFaces' depends on axioms: [propext,
---
126 Definitions/MMFLM86NegPairingFockStep.lean:222:4: error: Type mismatch
Definitions/MMFLM86NegPairingFockStep.lean:222:4: error: Type mismatch
  key (∑ i, (D i).osc.length) n D rfl
has type
  FaceAtFamily bL form E a b j m n D
but is expected to have type
  ∃ s,
    ∀ (i : Fin n),
      ((ZAligned bL form E) ((YFam bL form E a (-↑j - 1)) ((creationExpVL bL form b 0) (iotaVL b))) m)
          (stateOfVL bL form (D i)) =
        ∑ Q ∈ s,
          honestBlockCoeffJ form a b j m Q • (FLM86NPNA.blockOfShift bL form E a b j 0 m Q) (stateOfVL bL form (D i))
'MM.FLM86NPFS.FaceAtFamily' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
'MM.FLM86NPFS.honestNegPairingCoeffAtStates_iff_familyFaces' depends on axioms: [propext,
 sorryAx,
---
149 --- FAILED: Definitions/MMFLM86NegPairingFockStep.lean ---
