internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* Rew.toS.hom ((Rew.rewriteMap (Semiformula.fvListing σ)).hom ((Semiformula.lMap Φ) σ)) =
    ∀* Rew.toS.hom ((Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing).hom ((Semiformula.lMap Φ) σ))
Tactic:
simp [←Rew.hom_comp_app]
Proof state after:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* (Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ))).hom ((Semiformula.lMap Φ) σ) =
    ∀* (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing)).hom ((Semiformula.lMap Φ) σ)
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ (Semiformula.fvarList σ).length + 1 = ((Semiformula.lMap Φ) σ).fvarList.length + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ)) =
    (Rew.castLE ⋯).comp (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing))
Tactic:
ext x <;> simp [Rew.comp_app]
Proof state after:
case hb
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : Fin 0
⊢ Rew.toS #x = (Rew.castLE ⋯) (Rew.toS #x)

case hf
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ Semiformula.fvListing σ x = Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x)
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
case hb
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : Fin 0
⊢ Rew.toS #x = (Rew.castLE ⋯) (Rew.toS #x)
Tactic:
apply finZeroElim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
case hf
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ Semiformula.fvListing σ x = Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x)
Tactic:
ext
Proof state after:
case hf.h
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ ↑(Semiformula.fvListing σ x) = ↑(Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x))
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
case hf.h
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ ↑(Semiformula.fvListing σ x) = ↑(Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x))
Tactic:
simp [Semiformula.fvListing]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.open_iff
Proof state before:
L : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
n : ?m.1833779
n₁ n₂ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω.hom p).Open ↔ p.Open
Tactic:
induction p using Semiformula.rec' <;> try simp [Rew.rel, Rew.nrel, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.open_iff
Proof state before:
case hex
L : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
n : ?m.1833779
n₁ n₂ n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : ∀ (ω : Rew L ξ₁ (n✝ + 1) ξ₂ n₂), (ω.hom p✝).Open ↔ p✝.Open
ω : Rew L ξ₁ n✝ ξ₂ n₂
⊢ (ω.hom (∃' p✝)).Open ↔ (∃' p✝).Open
Tactic:
simp [Rew.rel, Rew.nrel, *]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.atom_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
a : α
⊢ V ⊧ atom a ↔ V a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.top_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
⊢ V ⊧ ⊤ ↔ True
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.bot_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
⊢ V ⊧ ⊥ ↔ False
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.and_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ V ⊧ p ⋏ q ↔ V ⊧ p ∧ V ⊧ q
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.or_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ V ⊧ p ⋎ q ↔ V ⊧ p ∨ V ⊧ q
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.imp_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ V ⊧ p ⟶ q ↔ V ⊧ p → V ⊧ q
Tactic:
simp
Proof state after:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ (∀ {w' : PUnit.{u_1 + 1}}, Satisfies (ClassicalModel V) w' p → Satisfies (ClassicalModel V) w' q) ↔
    Satisfies (ClassicalModel V) PUnit.unit p → Satisfies (ClassicalModel V) PUnit.unit q
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.imp_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ (∀ {w' : PUnit.{u_1 + 1}}, Satisfies (ClassicalModel V) w' p → Satisfies (ClassicalModel V) w' q) ↔
    Satisfies (ClassicalModel V) PUnit.unit p → Satisfies (ClassicalModel V) PUnit.unit q
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.neg_def
Proof state before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p : Formula α
⊢ V ⊧ ~p ↔ ¬V ⊧ p
Tactic:
simp only [NegAbbrev.neg, imp_def, bot_def]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.classical_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p ↔ V ⊧ p
Tactic:
simp [ValidOnModel]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ (∀ (w : (ClassicalModel V).World), Satisfies (ClassicalModel V) w p) ↔ Satisfies (ClassicalModel V) PUnit.unit p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.classical_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ (∀ (w : (ClassicalModel V).World), Satisfies (ClassicalModel V) w p) ↔ Satisfies (ClassicalModel V) PUnit.unit p
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnClassicalFrame_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p
Tactic:
intro h V
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ V ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnClassicalFrame_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ V ⊧ p
Tactic:
apply Formula.Kripke.ValidOnModel.classical_iff.mp
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnClassicalFrame_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p
Tactic:
exact h (by
  apply iff_definability_memAxiomSetFrameClass instClassicalDefinabilityExtensive |>.mpr;
  simp [Extensive];
) (ClassicalModel V).Valuation (ClassicalModel V).hereditary
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnClassicalFrame_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ (ClassicalModel V).Frame ∈ 𝔽(Ax(𝐂𝐥))
Tactic:
apply iff_definability_memAxiomSetFrameClass instClassicalDefinabilityExtensive |>.mpr
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ Extensive (ClassicalModel V).Frame.Rel
Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnClassicalFrame_iff
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ Extensive (ClassicalModel V).Frame.Rel
Tactic:
simp [Extensive]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.notClassicalValid_of_exists_ClassicalValuation
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ (∃ V, ¬V ⊧ p) → ¬𝔽(Ax(𝐂𝐥)) ⊧ p
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ ¬¬𝔽(Ax(𝐂𝐥)) ⊧ p → ¬∃ V, ¬V ⊧ p
Theorem: LO.Propositional.Superintuitionistic.notClassicalValid_of_exists_ClassicalValuation
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ ¬¬𝔽(Ax(𝐂𝐥)) ⊧ p → ¬∃ V, ¬V ⊧ p
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p
Theorem: LO.Propositional.Superintuitionistic.notClassicalValid_of_exists_ClassicalValuation
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p
Tactic:
apply Formula.Kripke.ValidOnClassicalFrame_iff
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.unprovable_classical_of_exists_ClassicalValuation
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ 𝐂𝐥 ⊬! p
Tactic:
apply not_imp_not.mpr $ Kripke.sound!
Proof state after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ¬𝔽(Ax(𝐂𝐥)) ⊧ p
Theorem: LO.Propositional.Superintuitionistic.unprovable_classical_of_exists_ClassicalValuation
Proof state before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ¬𝔽(Ax(𝐂𝐥)) ⊧ p
Tactic:
apply notClassicalValid_of_exists_ClassicalValuation
Proof state after:
case a
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ∃ V, ¬V ⊧ p
Theorem: LO.Propositional.Superintuitionistic.unprovable_classical_of_exists_ClassicalValuation
Proof state before:
case a
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : ∃ V, ¬V ⊧ p
⊢ ∃ V, ¬V ⊧ p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥
Tactic:
rintro p hp
Proof state after:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ p ∈ theory 𝐂𝐥
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ p ∈ theory 𝐂𝐥
Tactic:
simp [System.theory]
Proof state after:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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;
Proof 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✝
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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
Proof 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
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
⊢ ?m.28095
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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₂⟩)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.reducible_efq_dne
Proof 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
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~~p ↔ 𝐂𝐥 ⊢! p
Tactic:
constructor
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~~p → 𝐂𝐥 ⊢! p

case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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;
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐈𝐧𝐭 ⊢! ~~p → 𝐂𝐥 ⊢! p
Tactic:
intro d
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~~p
⊢ 𝐂𝐥 ⊢! p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐈𝐧𝐭 ⊢! ~~p
⊢ 𝐂𝐥 ⊢! p
Tactic:
exact dne'! $ reducible_efq_dne d
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
⊢ 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
Tactic:
intro d
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! p
⊢ 𝐈𝐧𝐭 ⊢! ~~p
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
case mpr.eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐂𝐥)
d : 𝐂𝐥 ⊢! p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Tactic:
simp at h
Proof 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✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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)
Proof 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✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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!;
Proof state after:
case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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);
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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;
Proof 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✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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
Proof 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
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ ?m.82229
Tactic:
simpa using hEFQ
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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;
Proof 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✝
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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
Proof 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
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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'!
Proof 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
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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!
Proof 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
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof state before:
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ ?m.83250
Tactic:
simpa using hLEM
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.iff_provable_dn_efq_dne_provable
Proof 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₂⟩
Proof state after:
no goals