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

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

State before:
F : Type
p : ConfigPartition
pc : PC F
⊢ ∀ (c : Config F) (a : PC F),
    ((∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a) →
      ∀ (a_1 : PC F), ((∃ x ∈ p.pcs, pc &&& x = a_1) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a_1) → c ∈ ⦃a⦄ → c ∈ ⦃a_1⦄ → a = a_1
Tactic:
intros c a h₀ b h₁ h₂ h₃
State after:
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ a = b

State before:
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ a = b
Tactic:
apply Or.elim h₀
State after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b

case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b

case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Tactic:
{
    intros h₄
    apply Exists.elim h₄
    intros x h₅
    simp [←h₅.right, semantics] at h₂
    apply Or.elim h₁
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
        simp at h₈
        simp[←h₅.right, ←h₇.right, h₈]
    }
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        apply Not.elim h₃.left h₂.left
    }
}
State after:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b

State before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Tactic:
{
    intros h₄
    apply Exists.elim h₄
    intros x h₅
    simp [←h₅.right, semantics] at h₂
    apply Or.elim h₁
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        apply Not.elim h₂.left h₃.left
    }
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
        simp at h₈
        simp[←h₅.right, ←h₇.right, h₈]
    }
}
State after:
no goals

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = a) → a = b
Tactic:
intros h₄
State after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ a = b

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ a = b
Tactic:
apply Exists.elim h₄
State after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = a → a = b

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = a → a = b
Tactic:
intros x h₅
State after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
⊢ a = b

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
⊢ a = b
Tactic:
simp [←h₅.right, semantics] at h₂
State after:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ a = b

State before:
case left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ a = b
Tactic:
apply Or.elim h₁
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b

case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b

case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
{
    intros h₆
    apply Exists.elim h₆
    intros y h₇
    simp[←h₇.right, semantics] at h₃
    have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
    simp at h₈
    simp[←h₅.right, ←h₇.right, h₈]
}
State after:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
{
    intros h₆
    apply Exists.elim h₆
    intros y h₇
    simp[←h₇.right, semantics] at h₃
    apply Not.elim h₃.left h₂.left
}
State after:
no goals

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b
Tactic:
intros h₆
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ a = b
Tactic:
apply Exists.elim h₆
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = b → a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = b → a = b
Tactic:
intros y h₇
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
⊢ a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
⊢ a = b
Tactic:
simp[←h₇.right, semantics] at h₃
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b
Tactic:
have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : { val := x, property := ⋯ } = { val := y, property := ⋯ }
⊢ a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : { val := x, property := ⋯ } = { val := y, property := ⋯ }
⊢ a = b
Tactic:
simp at h₈
State after:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : x = y
⊢ a = b

State before:
case left.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : x = y
⊢ a = b
Tactic:
simp[←h₅.right, ←h₇.right, h₈]
State after:
no goals

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
intros h₆
State after:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ a = b

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ a = b
Tactic:
apply Exists.elim h₆
State after:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = b → a = b

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = b → a = b
Tactic:
intros y h₇
State after:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
⊢ a = b

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
⊢ a = b
Tactic:
simp[←h₇.right, semantics] at h₃
State after:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b

State before:
case left.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ pc &&& x = a
h₂ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b
Tactic:
apply Not.elim h₃.left h₂.left
State after:
no goals

State before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
Tactic:
intros h₄
State after:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
⊢ a = b

State before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
⊢ a = b
Tactic:
apply Exists.elim h₄
State after:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = a → a = b

State before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = a → a = b
Tactic:
intros x h₅
State after:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
⊢ a = b

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

State before:
case right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ a = b
Tactic:
apply Or.elim h₁
State after:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b

case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b

case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
{
    intros h₆
    apply Exists.elim h₆
    intros y h₇
    simp[←h₇.right, semantics] at h₃
    apply Not.elim h₂.left h₃.left
}
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
{
    intros h₆
    apply Exists.elim h₆
    intros y h₇
    simp[←h₇.right, semantics] at h₃
    have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
    simp at h₈
    simp[←h₅.right, ←h₇.right, h₈]
}
State after:
no goals

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, pc &&& x = b) → a = b
Tactic:
intros h₆
State after:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ a = b

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ a = b
Tactic:
apply Exists.elim h₆
State after:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = b → a = b

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ pc &&& a_1 = b → a = b
Tactic:
intros y h₇
State after:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
⊢ a = b

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
⊢ a = b
Tactic:
simp[←h₇.right, semantics] at h₃
State after:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b

State before:
case right.left
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ pc &&& y = b
h₃ : c ∈ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b
Tactic:
apply Not.elim h₂.left h₃.left
State after:
no goals

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = b) → a = b
Tactic:
intros h₆
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ a = b
Tactic:
apply Exists.elim h₆
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = b → a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ ∀ (a_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = b → a = b
Tactic:
intros y h₇
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
⊢ a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₃ : c ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
⊢ a = b
Tactic:
simp[←h₇.right, semantics] at h₃
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b
Tactic:
have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : { val := x, property := ⋯ } = { val := y, property := ⋯ }
⊢ a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : { val := x, property := ⋯ } = { val := y, property := ⋯ }
⊢ a = b
Tactic:
simp at h₈
State after:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : x = y
⊢ a = b

State before:
case right.right
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
h₈ : x = y
⊢ a = b
Tactic:
simp[←h₅.right, ←h₇.right, h₈]
State after:
no goals