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

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p t)
Tactic:
simp [lindenbaum_next]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (if (𝓓)-Consistent (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2))

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (if (𝓓)-Consistent (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2))
Tactic:
split
State after:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)

State before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
. simpa;
State after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)

State before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
. have := consistent_either consistent p;
  simp_all only [false_or];
State after:
no goals

State before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : (𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (insert p t.1, t.2)
Tactic:
simpa
State after:
no goals

State before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
have := consistent_either consistent p
State after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
this : (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)

State before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t.1, t.2)
this : (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
⊢ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
simp_all only [false_or]
State after:
no goals