internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Tactic:
. intro h Γ Δ hΓ hΔ;
  by_contra hC;
  have : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj' := h hΓ (by simp; intro q hq; right; exact hΔ q hq);
  have : 𝓓 ⊢! Γ.conj' ⟶ (p :: Δ).disj' := implyRight_cons_disj'!.mpr hC;
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Tactic:
. intro h Γ Δ hΓ hΔ;
  simp_all;
  have : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (Δ.remove p).disj' := h hΓ (by
    intro q hq;
    have := by simpa using hΔ q $ List.mem_of_mem_remove hq;
    cases this with
    | inl h => simpa [h] using List.mem_remove_iff.mp hq;
    | inr h => assumption;
  );
  by_contra hC;
  have : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ (Δ.remove p).disj' := imp_trans! hC $ forthback_disj'_remove;
  contradiction;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
intro h Γ Δ hΓ hΔ
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
⊢ 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
⊢ 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
by_contra hC
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj' := h hΓ (by simp; intro q hq; right; exact hΔ q hq)
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
this : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
this : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj'
⊢ False
Tactic:
have : 𝓓 ⊢! Γ.conj' ⟶ (p :: Δ).disj' := implyRight_cons_disj'!.mpr hC
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
this✝ : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj'
this : 𝓓 ⊢! Γ.conj' ⟶ (p :: Δ).disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
this✝ : 𝓓 ⊬! Γ.conj' ⟶ (p :: Δ).disj'
this : 𝓓 ⊢! Γ.conj' ⟶ (p :: Δ).disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
⊢ ∀ p_1 ∈ p :: Δ, p_1 ∈ (T, insert p U).2
Tactic:
simp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ U
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ U
Tactic:
intro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q = p ∨ q ∈ U
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q = p ∨ q ∈ U
Tactic:
right
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q ∈ U
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : (𝓓)-Consistent (T, insert p U)
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p ∈ Δ, p ∈ U
hC : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
q : Formula α
hq : q ∈ Δ
⊢ q ∈ U
Tactic:
exact hΔ q hq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Tactic:
intro h Γ Δ hΓ hΔ
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ (T, insert p U).1
hΔ : ∀ p_1 ∈ Δ, p_1 ∈ (T, insert p U).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ (T, insert p U).1
hΔ : ∀ p_1 ∈ Δ, p_1 ∈ (T, insert p U).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
simp_all
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
have : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (Δ.remove p).disj' := h hΓ (by
  intro q hq;
  have := by simpa using hΔ q $ List.mem_of_mem_remove hq;
  cases this with
  | inl h => simpa [h] using List.mem_remove_iff.mp hq;
  | inr h => assumption;
)
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ (Δ.remove p).disj' := imp_trans! hC $ forthback_disj'_remove
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this✝ : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
this✝ : 𝓓 ⊬! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! Γ.conj' ⟶ p ⋎ (List.remove p Δ).disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
⊢ ∀ p_1 ∈ List.remove p Δ, p_1 ∈ U
Tactic:
intro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
⊢ q ∈ U
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
⊢ q ∈ U
Tactic:
have := by simpa using hΔ q $ List.mem_of_mem_remove hq;
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
this : q = p ∨ q ∈ U
⊢ q ∈ U
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
this : q = p ∨ q ∈ U
⊢ q ∈ U
Tactic:
cases this with
| inl h => simpa [h] using List.mem_remove_iff.mp hq;
| inr h => assumption;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
⊢ ?m.96897
Tactic:
simpa using hΔ q $ List.mem_of_mem_remove hq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h✝ : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
h : q = p
⊢ q ∈ U
Tactic:
simpa [h] using List.mem_remove_iff.mp hq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
h✝ : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! Γ.conj' ⟶ p ⋎ Δ.disj'
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
hΔ : ∀ p_1 ∈ Δ, p_1 = p ∨ p_1 ∈ U
q : Formula α
hq : q ∈ List.remove p Δ
h : q ∈ U
⊢ q ∈ U
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) ↔ ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
. contrapose; push_neg; apply iff_ParametricConsistent_insert₂.mpr;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
. contrapose; push_neg; apply iff_ParametricConsistent_insert₂.mp;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬¬(𝓓)-Consistent (T, insert p U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬¬(𝓓)-Consistent (T, insert p U)
Tactic:
push_neg
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Tactic:
apply iff_ParametricConsistent_insert₂.mpr
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
contrapose
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬¬(𝓓)-Consistent (T, insert p U) → ¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬¬(𝓓)-Consistent (T, insert p U) → ¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
push_neg
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
apply iff_ParametricConsistent_insert₂.mp
Proof state after:
no goals