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);
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞
no goals