internlm/Lean-Github huggingface dataset:
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⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
⊢ a = b
Tactic:
apply Exists.elim 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_1 : PC F), a_1 ∈ p.pcs ∧ ~~~pc &&& a_1 = 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⦄
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.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 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₃
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₄ : ∃ 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.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
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₄ : ∃ 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 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₈
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₄ : ∃ 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 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₈]
Proof state after:
no goals
Theorem: SPL.splitComplete
Proof 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]
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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)
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₀
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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⦄))
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₁
    )
)
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₀
            )
        )
    )
)
Proof state after:
no goals
Theorem: SPL.splitComplete
Proof 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₁
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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)
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₁
)
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₁
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₁
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₁
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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)
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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]
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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₀
        )
    )
)
Proof state after:
no goals
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄
Theorem: SPL.splitComplete
Proof 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
Proof 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⦄