Theorem: LO.Propositional.Superintuitionistic.iff_provable_neg_efq_provable_neg_efq (Logic/Propositional/Superintuitionistic/Deduction.lean)

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p ↔ 𝐂𝐥 ⊢! ~p
Tactic:
constructor
State after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p

case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p

State before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p

case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
. intro d; exact glivenko.mp $ dni'! d;
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
. intro d; exact tne'! $ glivenko.mpr d;
State after:
no goals

State before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~p → 𝐂𝐥 ⊢! ~p
Tactic:
intro d
State after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~p
⊢ 𝐂𝐥 ⊢! ~p

State before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~p
⊢ 𝐂𝐥 ⊢! ~p
Tactic:
exact glivenko.mp $ dni'! d
State after:
no goals

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! ~p → 𝐈𝐧𝐭 ⊢! ~p
Tactic:
intro d
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! ~p
⊢ 𝐈𝐧𝐭 ⊢! ~p

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! ~p
⊢ 𝐈𝐧𝐭 ⊢! ~p
Tactic:
exact tne'! $ glivenko.mpr d
State after:
no goals