Theorem: LO.Modal.Standard.normal_reducible (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
apply System.reducible_iff.mpr
State after:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
⊢ ∀ {f : Formula α}, 𝓓₁ ⊢! f → 𝓓₂ ⊢! f

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
State after:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p : Formula α
h : 𝓓₁ ⊢! p
⊢ 𝓓₂ ⊢! p

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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