Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_and (Logic/Modal/Standard/Kripke/Completeness.lean)

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
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

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;
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

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);
State after:
no goals

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
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

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
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

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
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

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;
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

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;
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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⟩
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

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
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

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)
State after:
no goals