internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
apply System.reducible_iff.mpr
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
⊢ ∀ {f : Formula α}, 𝓓₁ ⊢! f → 𝓓₂ ⊢! f
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
⊢ ∀ {f : Formula α}, 𝓓₁ ⊢! f → 𝓓₂ ⊢! f
Tactic:
intro p h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p : Formula α
h : 𝓓₁ ⊢! p
⊢ 𝓓₂ ⊢! p
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p : Formula α
h : 𝓓₁ ⊢! p
⊢ 𝓓₂ ⊢! p
Tactic:
induction h using Deduction.inducition_with_nec! with
| hMaxm hp => exact hMaxm hp;
| hMdp ihpq ihp => exact ihpq ⨀ ihp
| hNec ihp => exact Necessitation.nec! ihp
| _ =>
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ : Formula α
hp : p✝ ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p✝
Tactic:
exact hMaxm hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hMdp
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
hpq✝ : 𝓓₁ ⊢! p✝ ⟶ q✝
hp✝ : 𝓓₁ ⊢! p✝
ihpq : 𝓓₂ ⊢! p✝ ⟶ q✝
ihp : 𝓓₂ ⊢! p✝
⊢ 𝓓₂ ⊢! q✝
Tactic:
exact ihpq ⨀ ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hNec
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ : Formula α
hp✝ : 𝓓₁ ⊢! p✝
ihp : 𝓓₂ ⊢! p✝
⊢ 𝓓₂ ⊢! □p✝
Tactic:
exact Necessitation.nec! ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDne
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ : Formula α
⊢ 𝓓₂ ⊢! ~~p✝ ⟶ p✝
Tactic:
try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDne
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ : Formula α
⊢ 𝓓₂ ⊢! ~~p✝ ⟶ p✝
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hVerum
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p : Formula α
⊢ 𝓓₂ ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hImply₁
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hImply₂
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ r✝ : Formula α
⊢ 𝓓₂ ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hConj₁
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hConj₂
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hConj₃
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDisj₁
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDisj₂
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ : Formula α
⊢ 𝓓₂ ⊢! q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDisj₃
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ q✝ r✝ : Formula α
⊢ 𝓓₂ ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible
Proof state before:
case hDne
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p p✝ : Formula α
⊢ 𝓓₂ ⊢! ~~p✝ ⟶ p✝
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.normal_reducible_subset
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
apply normal_reducible
Proof state after:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
Theorem: LO.Modal.Standard.normal_reducible_subset
Proof state before:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
Tactic:
intro p hp
Proof state after:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
p : Formula α
hp : p ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p
Theorem: LO.Modal.Standard.normal_reducible_subset
Proof state before:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
p : Formula α
hp : p ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p
Tactic:
exact ⟨Deduction.maxm $ hSubset hp⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K_KT
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊 ≤ₛ 𝐊𝐓
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐊𝐓)
Theorem: LO.Modal.Standard.reducible_K_KT
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐊𝐓)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K_KD
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊 ≤ₛ 𝐊𝐃
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐊𝐃)
Theorem: LO.Modal.Standard.reducible_K_KD
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐊𝐃)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_KT_S4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝐓 ≤ₛ 𝐒𝟒
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝐓) ⊆ Ax(𝐒𝟒)
Theorem: LO.Modal.Standard.reducible_KT_S4
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝐓) ⊆ Ax(𝐒𝟒)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_S4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒 ≤ₛ 𝐒𝟒
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝟒) ⊆ Ax(𝐒𝟒)
Theorem: LO.Modal.Standard.reducible_K4_S4
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝟒) ⊆ Ax(𝐒𝟒)
Tactic:
intro
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
a✝ : Formula α
⊢ a✝ ∈ Ax(𝐊𝟒) → a✝ ∈ Ax(𝐒𝟒)
Theorem: LO.Modal.Standard.reducible_K4_S4
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
a✝ : Formula α
⊢ a✝ ∈ Ax(𝐊𝟒) → a✝ ∈ Ax(𝐒𝟒)
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_S4_S4Dot2
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐒𝟒 ≤ₛ 𝐒𝟒.𝟐
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒.𝟐)
Theorem: LO.Modal.Standard.reducible_S4_S4Dot2
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒.𝟐)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_S4_S4Dot3
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐒𝟒 ≤ₛ 𝐒𝟒.𝟑
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒.𝟑)
Theorem: LO.Modal.Standard.reducible_S4_S4Dot3
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒.𝟑)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_S4_S4Grz
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐒𝟒 ≤ₛ 𝐒𝟒𝐆𝐫𝐳
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒𝐆𝐫𝐳)
Theorem: LO.Modal.Standard.reducible_S4_S4Grz
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐒𝟒) ⊆ Ax(𝐒𝟒𝐆𝐫𝐳)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K_GL
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊 ≤ₛ 𝐆𝐋
Tactic:
apply normal_reducible_subset
Proof state after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐆𝐋)
Theorem: LO.Modal.Standard.reducible_K_GL
Proof state before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊) ⊆ Ax(𝐆𝐋)
Tactic:
simp only [Set.subset_union_left]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒 ≤ₛ 𝐓𝐫𝐢𝐯
Tactic:
apply normal_reducible
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒) → 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒) → 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
intro p hp
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒)
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒)
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
rcases hp with (hK | hFour)
Proof state after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐓𝐫𝐢𝐯 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐓𝐫𝐢𝐯 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hFour
Proof state after:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! Axioms.Four w✝
Theorem: LO.Modal.Standard.reducible_K4_Triv
Proof state before:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋
Tactic:
apply normal_reducible
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒) → 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {p : Formula α}, p ∈ Ax(𝐊𝟒) → 𝐆𝐋 ⊢! p
Tactic:
intro p hp
Proof state after:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒)
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hp : p ∈ Ax(𝐊𝟒)
⊢ 𝐆𝐋 ⊢! p
Tactic:
rcases hp with (hK | hFour)
Proof state after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Tactic:
. obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hK : p ∈ 𝗞
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p
⊢ 𝐆𝐋 ⊢! p
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
w✝¹ w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hFour : p ∈ 𝟰
⊢ 𝐆𝐋 ⊢! p
Tactic:
obtain ⟨_, _, e⟩ := hFour
Proof state after:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝
Theorem: LO.Modal.Standard.reducible_K4_GL
Proof state before:
case hMaxm.inr.intro.refl
α : Type u_1
inst✝ : DecidableEq α
w✝ : Formula α
⊢ 𝐆𝐋 ⊢! Axioms.Four w✝
Tactic:
exact axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)
Tactic:
apply System.reducible_iff.mpr
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐆𝐋 ⊢! f → 𝐊𝟒(𝐋) ⊢! f
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {f : Formula α}, 𝐆𝐋 ⊢! f → 𝐊𝟒(𝐋) ⊢! f
Tactic:
intro p h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Tactic:
induction h using Deduction.inducition! with
| hMaxm hp =>
  rcases hp with (hK | hL)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
  . obtain ⟨_, e⟩ := hL; subst_vars; exact axiomL!;
| hMdp ihpq ihp => exact ihpq ⨀ ihp;
| hNec _ ihp => exact Necessitation.nec! ihp;
| hLoeb _ ihp => exact LoebRule.loeb! ihp;
| hHenkin => simp_all only [Bool.false_eq_true];
| _ =>
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : p✝ ∈ Ax(𝐆𝐋)
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
rcases hp with (hK | hL)
Proof state after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
. obtain ⟨_, e⟩ := hL; subst_vars; exact axiomL!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.K w✝¹ w✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.K w✝¹ w✝
Tactic:
exact axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hL : p✝ ∈ 𝗟
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
obtain ⟨_, e⟩ := hL
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.L w✝
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! Axioms.L w✝
Tactic:
exact axiomL!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
hpq✝ : 𝐆𝐋 ⊢! p✝ ⟶ q✝
hp✝ : 𝐆𝐋 ⊢! p✝
ihpq : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
ihp : 𝐊𝟒(𝐋) ⊢! p✝
⊢ 𝐊𝟒(𝐋) ⊢! q✝
Tactic:
exact ihpq ⨀ ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasNec✝ : 𝐆𝐋.rules.nec = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! p✝
ihp : 𝐊𝟒(𝐋) ⊢! p✝
⊢ 𝐊𝟒(𝐋) ⊢! □p✝
Tactic:
exact Necessitation.nec! ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hLoeb
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasLoeb✝ : 𝐆𝐋.rules.loeb = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! □p✝ ⟶ p✝
ihp : 𝐊𝟒(𝐋) ⊢! □p✝ ⟶ p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
exact LoebRule.loeb! ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hHenkin
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
hasHenkin✝ : 𝐆𝐋.rules.henkin = true
p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢! □p✝ ⟷ p✝
a✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟷ p✝
⊢ 𝐊𝟒(𝐋) ⊢! p✝
Tactic:
simp_all only [Bool.false_eq_true]
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ~~p✝ ⟶ p✝
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.reducible_GL_K4Loeb
Proof state before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
⊢ 𝐊𝟒(𝐋) ⊢! p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
Proof state after:
no goals