Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical (Logic/Propositional/Superintuitionistic/Kripke/LEM.lean)

State before:
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 <ₛ 𝐂𝐥
Tactic:
constructor
State after:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭

State before:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Tactic:
. exact reducible_efq_dne;
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Tactic:
. apply reducible_iff.not.mpr;
  push_neg;
  obtain ⟨p, hp⟩ := noLEM (α := α);
  existsi (p ⋎ ~p);
  constructor;
  . exact lem!;
  . assumption;
State after:
no goals

State before:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥
Tactic:
exact reducible_efq_dne
State after:
no goals

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Tactic:
apply reducible_iff.not.mpr
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬∀ {f : Formula α}, 𝐂𝐥 ⊢! f → 𝐈𝐧𝐭 ⊢! f

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬∀ {f : Formula α}, 𝐂𝐥 ⊢! f → 𝐈𝐧𝐭 ⊢! f
Tactic:
push_neg
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Tactic:
obtain ⟨p, hp⟩ := noLEM (α := α)
State after:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f

State before:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Tactic:
existsi (p ⋎ ~p)
State after:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p ∧ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p

State before:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p ∧ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
constructor
State after:
case right.intro.left
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p

case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p

State before:
case right.intro.left
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p

case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
. exact lem!;
State after:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p

State before:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
. assumption;
State after:
no goals

State before:
case right.intro.left
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p
Tactic:
exact lem!
State after:
no goals

State before:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
assumption
State after:
no goals