internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
. intro Γ hΓ; exact h (by intro p hp; simp; right; exact hΓ p hp);
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ hΓ
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
exact h (by intro p hp; simp; left; exact hΓ p hp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ ∀ p ∈ Γ, p ∈ T₁ ∪ T₂
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Tactic:
simp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Tactic:
left
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁
Tactic:
exact hΓ p hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ hΓ
Proof state after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
exact h (by intro p hp; simp; right; exact hΓ p hp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ ∀ p ∈ Γ, p ∈ T₁ ∪ T₂
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Tactic:
simp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Tactic:
right
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₂
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₂
Tactic:
exact hΓ p hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_not_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂ → ¬(L)-Consistent (T₁ ∪ T₂)
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬¬(L)-Consistent (T₁ ∪ T₂) → ¬(¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂)
Theorem: LO.Modal.Standard.Theory.union_not_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬¬(L)-Consistent (T₁ ∪ T₂) → ¬(¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂)
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂
Theorem: LO.Modal.Standard.Theory.union_not_Lconsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂
Tactic:
exact union_ParametricConsistent
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T ↔ ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
. intro h Γ hΓ;
  by_contra hC;
  have : L ⊬! p ⋏ List.conj' Γ ⟶ ⊥ := implyLeft_cons_conj'!.not.mp $ @h (p :: Γ) (by
    rintro q hq;
    simp at hq;
    cases hq with
    | inl h => subst h; simp;
    | inr h => simp; right; exact hΓ q h;
  );
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
. intro h Γ hΓ;
  have := @h (Γ.remove p) (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 := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC;
  contradiction;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
intro h Γ hΓ
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
⊢ L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
⊢ L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊬! p ⋏ List.conj' Γ ⟶ ⊥ := implyLeft_cons_conj'!.not.mp $ @h (p :: Γ) (by
  rintro q hq;
  simp at hq;
  cases hq with
  | inl h => subst h; simp;
  | inr h => simp; right; exact hΓ q h;
)
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
this : L ⊬! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
this : L ⊬! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∀ p_1 ∈ p :: Γ, p_1 ∈ insert p T
Tactic:
rintro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ p :: Γ
⊢ q ∈ insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ p :: Γ
⊢ q ∈ insert p T
Tactic:
simp at hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q = p ∨ q ∈ Γ
⊢ q ∈ insert p T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q = p ∨ q ∈ Γ
⊢ q ∈ insert p T
Tactic:
cases hq with
| inl h => subst h; simp;
| inr h => simp; right; exact hΓ q h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q = p
⊢ q ∈ insert p T
Tactic:
subst h
Proof state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
q : Formula α
h : (L)-Consistent insert q T
hC : L ⊢! q ⋏ Γ.conj' ⟶ ⊥
⊢ q ∈ insert q T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
q : Formula α
h : (L)-Consistent insert q T
hC : L ⊢! q ⋏ Γ.conj' ⟶ ⊥
⊢ q ∈ insert q T
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ insert p T
Tactic:
simp
Proof state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q = p ∨ q ∈ T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q = p ∨ q ∈ T
Tactic:
right
Proof state after:
case inr.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case inr.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ q h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
intro h Γ hΓ
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
have := @h (Γ.remove p) (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 α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this✝ : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this✝ : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ ∀ q ∈ List.remove p Γ, q ∈ T
Tactic:
intro q hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ q ∈ T
Tactic:
have := by simpa using hΓ q $ List.mem_of_mem_remove hq;
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
this : q = p ∨ q ∈ T
⊢ q ∈ T
Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
this : q = p ∨ q ∈ T
⊢ q ∈ T
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.Modal.Standard.Theory.iff_insert_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ ?m.55194
Tactic:
simpa using hΓ q $ List.mem_of_mem_remove hq
Proof state after:
no goals