Theorem: Execution.State.Over.exists_allowed_of_acyclic_has_unprocessed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr : α
s : State.Over rtr
_x✝ :
  (i : Component.idType Component.rcn) ×'
    (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝⁴ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y _x✝ →
      ∃ i, Allows s.toState i
i : Component.idType Component.rcn
a✝³ : (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝² :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := a✝³ } →
      ∃ i, Allows s.toState i
a : Dependency.Acyclic rtr
h₁✝¹ : (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝¹ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := h₁✝¹ } } →
      ∃ i, Allows s.toState i
h₁✝ : i ∈ s.rtr[Component.rcn]
h₂✝ : i ∉ s.progress
a✝ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } } →
      ∃ i, Allows s.toState i
h : ¬dependencies s.rtr i \ s.progress = ∅
w✝ : ID
hd : w✝ ∈ dependencies s.rtr i \ s.progress
h₁ : w✝ ∈ dependencies s.rtr i
h₂ : w✝ ∉ s.progress
⊢ (Set.Finite.toFinset ⋯).card < (Set.Finite.toFinset ⋯).card
Tactic:
refine Finset.card_lt_card $ Set.Finite.toFinset_strictMono ?_
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr : α
s : State.Over rtr
_x✝ :
  (i : Component.idType Component.rcn) ×'
    (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝⁴ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y _x✝ →
      ∃ i, Allows s.toState i
i : Component.idType Component.rcn
a✝³ : (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝² :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := a✝³ } →
      ∃ i, Allows s.toState i
a : Dependency.Acyclic rtr
h₁✝¹ : (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝¹ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := h₁✝¹ } } →
      ∃ i, Allows s.toState i
h₁✝ : i ∈ s.rtr[Component.rcn]
h₂✝ : i ∉ s.progress
a✝ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } } →
      ∃ i, Allows s.toState i
h : ¬dependencies s.rtr i \ s.progress = ∅
w✝ : ID
hd : w✝ ∈ dependencies s.rtr i \ s.progress
h₁ : w✝ ∈ dependencies s.rtr i
h₂ : w✝ ∉ s.progress
⊢ dependencies s.rtr w✝ \ s.progress ⊂ dependencies s.rtr i \ s.progress