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

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥
Tactic:
rintro p hp
State after:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ p ∈ theory 𝐂𝐥

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ p ∈ theory 𝐂𝐥
Tactic:
simp [System.theory]
State after:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p
Tactic:
induction hp.some with
| eaxm h =>
  obtain ⟨q, hq⟩ := by simpa using h;
  subst hq;
  apply efq!;
| mdp h₁ h₂ ih₁ ih₂ => exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| _ => simp;
State after:
no goals

State before:
case eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p✝
Tactic:
obtain ⟨q, hq⟩ := by simpa using h;
State after:
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐂𝐥 ⊢! p✝

State before:
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐂𝐥 ⊢! p✝
Tactic:
subst hq
State after:
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
h : Axioms.EFQ q ∈ Ax(𝐈𝐧𝐭)
hp : Axioms.EFQ q ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! Axioms.EFQ q

State before:
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
h : Axioms.EFQ q ∈ Ax(𝐈𝐧𝐭)
hp : Axioms.EFQ q ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! Axioms.EFQ q
Tactic:
apply efq!
State after:
no goals

State before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
⊢ ?m.28095
Tactic:
simpa using h
State after:
no goals

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

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