internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
Tactic:
intro hp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
⊢ ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
have := provable_iff_insert_neg_not_Lconsistent.not.mp $ membership_iff.not.mp hp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this : ¬¬(L)-Consistent insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this : ¬¬(L)-Consistent insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
have := (not_imp_not.mpr $ Ω.maximal (U := insert (~p) Ω.theory)) this
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : ¬Ω.theory ⊂ insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : ¬Ω.theory ⊂ insert (~p) Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
simp [Set.ssubset_def] at this
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
apply this
Proof state after:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ insert (p ⟶ ⊥) Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_neg
Proof state before:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
hp : p ∉ Ω.theory
this✝ : ¬¬(L)-Consistent insert (~p) Ω.theory
this : insert (p ⟶ ⊥) Ω.theory ⊆ Ω.theory
⊢ ~p ∈ insert (p ⟶ ⊥) Ω.theory
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~~p ∈ Ω.theory ↔ p ∈ Ω.theory
Tactic:
simp [membership_iff]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ ↔ Ω.theory *⊢[L]! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ ↔ Ω.theory *⊢[L]! p
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
. intro h; exact dne'! h;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
. intro h; exact dni'! h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! p
Tactic:
exact dne'! h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
exact dni'! h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⟶ q ∈ Ω.theory ↔ p ∈ Ω.theory → q ∈ Ω.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⟶ q ∈ Ω.theory → p ∈ Ω.theory → q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ (p ∈ Ω.theory → q ∈ Ω.theory) → p ⟶ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⟶ q ∈ Ω.theory → p ∈ Ω.theory → q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ (p ∈ Ω.theory → q ∈ Ω.theory) → p ⟶ q ∈ Ω.theory
Tactic:
. intro hpq hp;
  replace dpq := membership_iff.mp hpq;
  replace dp  := membership_iff.mp hp;
  apply membership_iff.mpr;
  exact dpq ⨀ dp;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ (p ∈ Ω.theory → q ∈ Ω.theory) → p ⟶ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ (p ∈ Ω.theory → q ∈ Ω.theory) → p ⟶ q ∈ Ω.theory
Tactic:
. intro h;
  replace h : p ∉ Ω.theory ∨ q ∈ Ω.theory := or_iff_not_imp_left.mpr (by simpa using h);
  cases h with
  | inl h =>
    apply membership_iff.mpr;
    exact efq_of_neg! $ membership_iff.mp $ iff_mem_neg.mpr h;
  | inr h =>
    apply membership_iff.mpr;
    exact imply₁! ⨀ (membership_iff.mp h)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⟶ q ∈ Ω.theory → p ∈ Ω.theory → q ∈ Ω.theory
Tactic:
intro hpq hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
⊢ q ∈ Ω.theory
Tactic:
replace dpq := membership_iff.mp hpq
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
⊢ q ∈ Ω.theory
Tactic:
replace dp  := membership_iff.mp hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
dp : Ω.theory *⊢[L]! p
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
dp : Ω.theory *⊢[L]! p
⊢ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
dp : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⟶ q ∈ Ω.theory
hp : p ∈ Ω.theory
dpq : Ω.theory *⊢[L]! p ⟶ q
dp : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! q
Tactic:
exact dpq ⨀ dp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ (p ∈ Ω.theory → q ∈ Ω.theory) → p ⟶ q ∈ Ω.theory
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∈ Ω.theory → q ∈ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∈ Ω.theory → q ∈ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Tactic:
replace h : p ∉ Ω.theory ∨ q ∈ Ω.theory := or_iff_not_imp_left.mpr (by simpa using h)
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∉ Ω.theory ∨ q ∈ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∉ Ω.theory ∨ q ∈ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Tactic:
cases h with
| inl h =>
  apply membership_iff.mpr;
  exact efq_of_neg! $ membership_iff.mp $ iff_mem_neg.mpr h;
| inr h =>
  apply membership_iff.mpr;
  exact imply₁! ⨀ (membership_iff.mp h)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∈ Ω.theory → q ∈ Ω.theory
⊢ ¬p ∉ Ω.theory → q ∈ Ω.theory
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∉ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∉ Ω.theory
⊢ Ω.theory *⊢[L]! p ⟶ q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : p ∉ Ω.theory
⊢ Ω.theory *⊢[L]! p ⟶ q
Tactic:
exact efq_of_neg! $ membership_iff.mp $ iff_mem_neg.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω.theory
⊢ p ⟶ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⟶ q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_imp
Proof state before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⟶ q
Tactic:
exact imply₁! ⨀ (membership_iff.mp h)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋏ q ∈ Ω.theory ↔ p ∈ Ω.theory ∧ q ∈ Ω.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋏ q ∈ Ω.theory → p ∈ Ω.theory ∧ q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory → p ⋏ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋏ q ∈ Ω.theory → p ∈ Ω.theory ∧ q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory → p ⋏ q ∈ Ω.theory
Tactic:
. intro hpq;
  replace hpq := membership_iff.mp hpq;
  constructor;
  . apply membership_iff.mpr; exact conj₁'! hpq;
  . apply membership_iff.mpr; exact conj₂'! hpq;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory → p ⋏ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory → p ⋏ q ∈ Ω.theory
Tactic:
. rintro ⟨hp, hq⟩;
  apply membership_iff.mpr;
  exact conj₃'! (membership_iff.mp hp) (membership_iff.mp hq);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋏ q ∈ Ω.theory → p ∈ Ω.theory ∧ q ∈ Ω.theory
Tactic:
intro hpq
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋏ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋏ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory
Tactic:
replace hpq := membership_iff.mp hpq
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory
Tactic:
constructor
Proof state after:
case mp.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ p ∈ Ω.theory

case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ p ∈ Ω.theory

case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr; exact conj₁'! hpq;
Proof state after:
case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr; exact conj₂'! hpq;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ p ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mp.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ Ω.theory *⊢[L]! p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ Ω.theory *⊢[L]! p
Tactic:
exact conj₁'! hpq
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ Ω.theory *⊢[L]! q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mp.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⋏ q
⊢ Ω.theory *⊢[L]! q
Tactic:
exact conj₂'! hpq
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∧ q ∈ Ω.theory → p ⋏ q ∈ Ω.theory
Tactic:
rintro ⟨hp, hq⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
hq : q ∈ Ω.theory
⊢ p ⋏ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
hq : q ∈ Ω.theory
⊢ p ⋏ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋏ q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and
Proof state before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋏ q
Tactic:
exact conj₃'! (membership_iff.mp hp) (membership_iff.mp hq)
Proof state after:
no goals