Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ ∃ u, t ⊆ u ∧ (𝓓)-Consistent u ∧ u.Saturated
Tactic:
use t∞
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞ ∧ (𝓓)-Consistent t∞ ∧ t∞.Saturated

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞ ∧ (𝓓)-Consistent t∞ ∧ t∞.Saturated
Tactic:
refine ⟨?subset, ?consistent, ?saturated⟩
State after:
case subset
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞

case consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞

case saturated
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t∞.Saturated

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞
Tactic:
case subset => constructor <;> apply Set.subset_iUnion_of_subset 0 (by simp);
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t∞.Saturated
Tactic:
case saturated =>
  intro p;
  cases mem_lindenbaum_next_indexed t p with
  | inl h => left; simp [lindenbaum_maximal]; use (encode p + 1);
  | inr h => right; simp [lindenbaum_maximal]; use (encode p + 1);
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞
Tactic:
case consistent =>
  intro Γ Δ hΓ hΔ;
  simp_all [lindenbaum_maximal];
  obtain ⟨m, hΓ⟩ : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1 := by
    induction Γ with
    | nil => simp;
    | cons p Γ ih =>
      simp_all;
      obtain ⟨i, hi⟩ := hΓ.1;
      obtain ⟨m, hm⟩ := ih;
      use (i + m);
      constructor;
      . exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
      . intro q hq;
        exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
  obtain ⟨n, hΔ⟩ : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2 := by
    induction Δ with
    | nil => simp;
    | cons p Δ ih =>
      simp_all;
      obtain ⟨i, hi⟩ := hΔ.1;
      obtain ⟨n, hn⟩ := ih;
      use (i + n);
      constructor;
      . exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
      . intro q hq;
        exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
  rcases (lt_trichotomy m n) with hm | hmn | hn;
  . exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ;
  . subst hmn;
    exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ;
  . exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ (by intro p hp; exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp);
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞
Tactic:
constructor <;> apply Set.subset_iUnion_of_subset 0 (by simp)
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t.2 ⊆ t[0].2
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t∞.Saturated
Tactic:
intro p
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
cases mem_lindenbaum_next_indexed t p with
| inl h => left; simp [lindenbaum_maximal]; use (encode p + 1);
| inr h => right; simp [lindenbaum_maximal]; use (encode p + 1);
State after:
no goals

State before:
case inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
left
State after:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1

State before:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1
Tactic:
simp [lindenbaum_maximal]
State after:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ ∃ i, p ∈ t[i].1

State before:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ ∃ i, p ∈ t[i].1
Tactic:
use (encode p + 1)
State after:
no goals

State before:
case inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
right
State after:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.2

State before:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.2
Tactic:
simp [lindenbaum_maximal]
State after:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ ∃ i, p ∈ t[i].2

State before:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ ∃ i, p ∈ t[i].2
Tactic:
use (encode p + 1)
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞
Tactic:
intro Γ Δ hΓ hΔ
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t∞.1
hΔ : ∀ p ∈ Δ, p ∈ t∞.2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t∞.1
hΔ : ∀ p ∈ Δ, p ∈ t∞.2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
simp_all [lindenbaum_maximal]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨m, hΓ⟩ : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1 := by
  induction Γ with
  | nil => simp;
  | cons p Γ ih =>
    simp_all;
    obtain ⟨i, hi⟩ := hΓ.1;
    obtain ⟨m, hm⟩ := ih;
    use (i + m);
    constructor;
    . exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
    . intro q hq;
      exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
State after:
case intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨n, hΔ⟩ : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2 := by
  induction Δ with
  | nil => simp;
  | cons p Δ ih =>
    simp_all;
    obtain ⟨i, hi⟩ := hΔ.1;
    obtain ⟨n, hn⟩ := ih;
    use (i + n);
    constructor;
    . exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
    . intro q hq;
      exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
State after:
case intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
rcases (lt_trichotomy m n) with hm | hmn | hn
State after:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ;
State after:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. subst hmn;
  exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ;
State after:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ (by intro p hp; exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp);
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
⊢ ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
Tactic:
induction Γ with
| nil => simp;
| cons p Γ ih =>
  simp_all;
  obtain ⟨i, hi⟩ := hΓ.1;
  obtain ⟨m, hm⟩ := ih;
  use (i + m);
  constructor;
  . exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
  . intro q hq;
    exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
State after:
no goals

State before:
case nil
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
hΓ : ∀ p ∈ [], ∃ i, p ∈ t[i].1
⊢ ∃ m, ∀ p ∈ [], p ∈ t[m].1
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : (∀ p ∈ Γ, ∃ i, p ∈ t[i].1) → ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : ∀ p_1 ∈ p :: Γ, ∃ i, p_1 ∈ t[i].1
⊢ ∃ m, ∀ p_1 ∈ p :: Γ, p_1 ∈ t[m].1
Tactic:
simp_all
State after:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1

State before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
obtain ⟨i, hi⟩ := hΓ.1
State after:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1

State before:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
obtain ⟨m, hm⟩ := ih
State after:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1

State before:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
use (i + m)
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1 ∧ ∀ a ∈ Γ, a ∈ t[i + m].1

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1 ∧ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1

State before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
. exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
State after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
. intro q hq;
  exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ i ≤ i + m
Tactic:
simp
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
intro q hq
State after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ q ∈ t[i + m].1

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ q ∈ t[i + m].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ m ≤ i + m
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
Tactic:
induction Δ with
| nil => simp;
| cons p Δ ih =>
  simp_all;
  obtain ⟨i, hi⟩ := hΔ.1;
  obtain ⟨n, hn⟩ := ih;
  use (i + n);
  constructor;
  . exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
  . intro q hq;
    exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
State after:
no goals

State before:
case nil
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
hΔ : ∀ p ∈ [], ∃ i, p ∈ t[i].2
⊢ ∃ n, ∀ p ∈ [], p ∈ t[n].2
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : (∀ p ∈ Δ, ∃ i, p ∈ t[i].2) → ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : ∀ p_1 ∈ p :: Δ, ∃ i, p_1 ∈ t[i].2
⊢ ∃ n, ∀ p_1 ∈ p :: Δ, p_1 ∈ t[n].2
Tactic:
simp_all
State after:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2

State before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
obtain ⟨i, hi⟩ := hΔ.1
State after:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2

State before:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
obtain ⟨n, hn⟩ := ih
State after:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2

State before:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
use (i + n)
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2 ∧ ∀ a ∈ Δ, a ∈ t[i + n].2

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2 ∧ ∀ a ∈ Δ, a ∈ t[i + n].2
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2

State before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2
Tactic:
. exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
State after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2
Tactic:
. intro q hq;
  exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2
Tactic:
exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ i ≤ i + n
Tactic:
simp
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2
Tactic:
intro q hq
State after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
q : Formula α
hq : q ∈ Δ
⊢ q ∈ t[i + n].2

State before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
q : Formula α
hq : q ∈ Δ
⊢ q ∈ t[i + n].2
Tactic:
exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
q : Formula α
hq : q ∈ Δ
⊢ n ≤ i + n
Tactic:
simp
State after:
no goals

State before:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ ∀ p ∈ Γ, p ∈ t[n].1
Tactic:
intro p hp
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
p : Formula α
hp : p ∈ Γ
⊢ p ∈ t[n].1

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
p : Formula α
hp : p ∈ Γ
⊢ p ∈ t[n].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp
State after:
no goals

State before:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
subst hmn
State after:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
hΔ : ∀ p ∈ Δ, p ∈ t[m].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
hΔ : ∀ p ∈ Δ, p ∈ t[m].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ
State after:
no goals

State before:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ (by intro p hp; exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp)
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ ∀ p ∈ Δ, p ∈ t[m].2
Tactic:
intro p hp
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
p : Formula α
hp : p ∈ Δ
⊢ p ∈ t[m].2

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
p : Formula α
hp : p ∈ Δ
⊢ p ∈ t[m].2
Tactic:
exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp
State after:
no goals