internlm/Lean-Github huggingface dataset:
Theorem: SPL.splitDisjoint
Proof 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₁
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₈]
}
Proof 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
Theorem: SPL.splitDisjoint
Proof 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
}
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₇
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₃
Proof 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
Theorem: SPL.splitDisjoint
Proof 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
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₈
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₈]
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₇
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₃
Proof 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
Theorem: SPL.splitDisjoint
Proof 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
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof 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₄
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₄
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₅
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₂
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₁
Proof 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
Theorem: SPL.splitDisjoint
Proof 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
}
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₈]
}
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₇
Proof 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
Theorem: SPL.splitDisjoint
Proof 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₃
Proof 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
Theorem: SPL.splitDisjoint
Proof 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
Proof state after:
no goals
Theorem: SPL.splitDisjoint
Proof 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₆
Proof 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