Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable (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 dne'! $ reducible_efq_dne 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;
  induction d.some with
  | eaxm h =>
    simp at h;
    rcases h with (hEFQ | hLEM);
    . obtain ⟨q, hq⟩ := by simpa using hEFQ;
      subst hq;
      exact dni'! efq!;
    . obtain ⟨q, hq⟩ := by simpa using hLEM;
      subst hq;
      apply FiniteContext.deduct'!;
      have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!;
      exact (conj₂'! this) ⨀ (conj₁'! this);
  | @mdp p q h₁ h₂ ih₁ ih₂ =>
    exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩;
  | _ => apply dni'!; simp;
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 dne'! $ reducible_efq_dne 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:
induction d.some with
| eaxm h =>
  simp at h;
  rcases h with (hEFQ | hLEM);
  . obtain ⟨q, hq⟩ := by simpa using hEFQ;
    subst hq;
    exact dni'! efq!;
  . obtain ⟨q, hq⟩ := by simpa using hLEM;
    subst hq;
    apply FiniteContext.deduct'!;
    have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!;
    exact (conj₂'! this) ⨀ (conj₁'! this);
| @mdp p q h₁ h₂ ih₁ ih₂ =>
  exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩;
| _ => apply dni'!; simp;
State after:
no goals

State before:
case mpr.eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐂𝐥)
d : 𝐂𝐥 ⊢! p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
simp at h
State after:
case mpr.eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
h : (∃ p, Axioms.EFQ p = p✝) ∨ ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

State before:
case mpr.eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
h : (∃ p, Axioms.EFQ p = p✝) ∨ ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
rcases h with (hEFQ | hLEM)
State after:
case mpr.eaxm.inl
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

State before:
case mpr.eaxm.inl
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
. obtain ⟨q, hq⟩ := by simpa using hEFQ;
  subst hq;
  exact dni'! efq!;
State after:
case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

State before:
case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
. obtain ⟨q, hq⟩ := by simpa using hLEM;
  subst hq;
  apply FiniteContext.deduct'!;
  have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!;
  exact (conj₂'! this) ⨀ (conj₁'! this);
State after:
no goals

State before:
case mpr.eaxm.inl
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
obtain ⟨q, hq⟩ := by simpa using hEFQ;
State after:
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

State before:
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
subst hq
State after:
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.EFQ q
hEFQ : ∃ p, Axioms.EFQ p = Axioms.EFQ q
⊢ 𝐈𝐧𝐭 ⊢! ~~Axioms.EFQ q

State before:
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.EFQ q
hEFQ : ∃ p, Axioms.EFQ p = Axioms.EFQ q
⊢ 𝐈𝐧𝐭 ⊢! ~~Axioms.EFQ q
Tactic:
exact dni'! efq!
State after:
no goals

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ ?m.82229
Tactic:
simpa using hEFQ
State after:
no goals

State before:
case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
obtain ⟨q, hq⟩ := by simpa using hLEM;
State after:
case mpr.eaxm.inr.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
q : Formula α
hq : Axioms.LEM q = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

State before:
case mpr.eaxm.inr.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
q : Formula α
hq : Axioms.LEM q = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
subst hq
State after:
case mpr.eaxm.inr.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
⊢ 𝐈𝐧𝐭 ⊢! ~~Axioms.LEM q

State before:
case mpr.eaxm.inr.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
⊢ 𝐈𝐧𝐭 ⊢! ~~Axioms.LEM q
Tactic:
apply FiniteContext.deduct'!
State after:
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum

State before:
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum
Tactic:
have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!
State after:
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
this : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum

State before:
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
this : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum
Tactic:
exact (conj₂'! this) ⨀ (conj₁'! this)
State after:
no goals

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ ?m.83250
Tactic:
simpa using hLEM
State after:
no goals

State before:
case mpr.mdp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p✝ p q : Formula α
h₁ : Deduction 𝐂𝐥 (p ⟶ q)
h₂ : Deduction 𝐂𝐥 p
ih₁ : 𝐂𝐥 ⊢! p ⟶ q → 𝐈𝐧𝐭 ⊢! ~~(p ⟶ q)
ih₂ : 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
d : 𝐂𝐥 ⊢! q
⊢ 𝐈𝐧𝐭 ⊢! ~~q
Tactic:
exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩
State after:
no goals

State before:
case mpr.disj₃
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! ~~((p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝)
Tactic:
apply dni'!
State after:
case mpr.disj₃.b
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝

State before:
case mpr.disj₃.b
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ q✝ r✝ : Formula α
d : 𝐂𝐥 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐈𝐧𝐭 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
simp
State after:
no goals