Theorem: SPL.splitComplete (Var/SPL.lean)

State before:
F : Type
p : ConfigPartition
splitter : PC F
⊢ completePCs (Set.split (PC F) p.pcs fun p => (splitter &&& p, ~~~splitter &&& p))
Tactic:
simp[Set.split, completePCs]
State after:
F : Type
p : ConfigPartition
splitter : PC F
⊢ ∀ (c : Config F), ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
F : Type
p : ConfigPartition
splitter : PC F
⊢ ∀ (c : Config F), ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
intros c
State after:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Exists.elim (p.complete c)
State after:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
⊢ ∀ (a : ↑p.pcs), c ∈ ⦃↑a⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
⊢ ∀ (a : ↑p.pcs), c ∈ ⦃↑a⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
intros x h₀
State after:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Or.elim (Classical.em (c ∈ ⦃splitter &&& x.val⦄))
State after:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
(
    intros h₁
    apply Exists.intro (splitter &&& x)
    apply And.intro
    (
        apply Or.intro_left
        apply Exists.intro ↑x
        simp
        exact h₁
    )
)
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
(
    intro h₁
    simp[semantics] at h₁
    apply Exists.intro (~~~splitter &&& x)
    simp[semantics]
    apply And.intro
    (
        apply Or.intro_right
        apply Exists.intro ↑x
        apply And.intro
        (
            simp
            simp
            apply And.intro
            (
                apply Classical.byContradiction
                intros h₂
                simp at h₂
                apply h₁ h₂
                exact h₀
                exact h₀
            )
        )
    )
)
State after:
no goals

State before:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
intros h₁
State after:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Exists.intro (splitter &&& x)
State after:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = splitter &&& ↑x) ∧
    c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = splitter &&& ↑x) ∧
    c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply And.intro
State after:
case left.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
(
    apply Or.intro_left
    apply Exists.intro ↑x
    simp
    exact h₁
)
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Or.intro_left
State after:
case left.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ∃ x_1 ∈ p.pcs, splitter &&& x_1 = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Exists.intro ↑x
State after:
case left.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ↑x ∈ p.pcs ∧ splitter &&& ↑x = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ ↑x ∈ p.pcs ∧ splitter &&& ↑x = splitter &&& ↑x

case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
simp
State after:
case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case left.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter &&& ↑x⦄
⊢ c ∈ ⦃splitter &&& ↑x⦄

case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
exact h₁
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
intro h₁
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∉ ⦃splitter &&& ↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∉ ⦃splitter &&& ↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
simp[semantics] at h₁
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
Tactic:
apply Exists.intro (~~~splitter &&& x)
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x) ∧
    c ∈ ⦃~~~splitter &&& ↑x⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x) ∧
    c ∈ ⦃~~~splitter &&& ↑x⦄
Tactic:
simp[semantics]
State after:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x) ∧
    c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ((∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x) ∧
    c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply And.intro
State after:
case right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
(
    apply Or.intro_right
    apply Exists.intro ↑x
    apply And.intro
    (
        simp
        simp
        apply And.intro
        (
            apply Classical.byContradiction
            intros h₂
            simp at h₂
            apply h₁ h₂
            exact h₀
            exact h₀
        )
    )
)
State after:
no goals

State before:
case right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply Or.intro_right
State after:
case right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply Exists.intro ↑x
State after:
case right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs ∧ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs ∧ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply And.intro
State after:
case right.left.h.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs

case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.left.h.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs

case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
(
    simp
    simp
    apply And.intro
    (
        apply Classical.byContradiction
        intros h₂
        simp at h₂
        apply h₁ h₂
        exact h₀
        exact h₀
    )
)
State after:
no goals

State before:
case right.left.h.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ↑x ∈ p.pcs

case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
simp
State after:
case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
simp
State after:
case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄

State before:
case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
Tactic:
apply And.intro
State after:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
(
    apply Classical.byContradiction
    intros h₂
    simp at h₂
    apply h₁ h₂
    exact h₀
    exact h₀
)
State after:
no goals

State before:
case right.right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
apply Classical.byContradiction
State after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ¬c ∉ ⦃splitter⦄ → False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ¬c ∉ ⦃splitter⦄ → False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
intros h₂
State after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : ¬c ∉ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : ¬c ∉ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
simp at h₂
State after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ False

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
apply h₁ h₂
State after:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ c ∈ ⦃↑x⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.left.h
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
h₂ : c ∈ ⦃splitter⦄
⊢ c ∈ ⦃↑x⦄

case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
exact h₀
State after:
case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄

State before:
case right.right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∈ ⦃↑x⦄
Tactic:
exact h₀
State after:
no goals