internlm/Lean-Github huggingface dataset:
Theorem: Finset.map_disj_union
Proof state before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩);
  . use a₁; simp_all;
  . use a₂; simp_all;
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
rintro ⟨a, h₁ | h₂, hb⟩
Proof state after:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
. left; use a;
Proof state after:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
. right; use a;
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
left
Proof state after:
case mp.intro.intro.inl.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ ∃ a ∈ s₁, f a
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inl.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ ∃ a ∈ s₁, f a
Tactic:
use a
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
right
Proof state after:
case mp.intro.intro.inr.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ ∃ a ∈ s₂, f a
Theorem: Finset.map_disj_union
Proof state before:
case mp.intro.intro.inr.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ ∃ a ∈ s₂, f a
Tactic:
use a
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩)
Proof state after:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Theorem: Finset.map_disj_union
Proof state before:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. use a₁; simp_all;
Proof state after:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Theorem: Finset.map_disj_union
Proof state before:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. use a₂; simp_all;
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
use a₁
Proof state after:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ (a₁ ∈ s₁ ∨ a₁ ∈ s₂) ∧ f a₁
Theorem: Finset.map_disj_union
Proof state before:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ (a₁ ∈ s₁ ∨ a₁ ∈ s₂) ∧ f a₁
Tactic:
simp_all
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
use a₂
Proof state after:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ (a₂ ∈ s₁ ∨ a₂ ∈ s₂) ∧ f a₂
Theorem: Finset.map_disj_union
Proof state before:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ (a₂ ∈ s₁ ∨ a₂ ∈ s₂) ∧ f a₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.le_eq
Proof state before:
L : Language
inst✝¹ : Operator.Eq L
inst✝ : Operator.LT L
μ : Type u_1
n : ℕ
t₁ t₂ : Semiterm L μ n
⊢ LT.le.operator ![t₁, t₂] = (“(!!t₁ = !!t₂ ∨ !!t₁ < !!t₂)”)
Tactic:
simp [Operator.operator, Operator.or, LT.le, ←Rew.hom_comp_app, ←Matrix.fun_eq_vec₂]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_atom
Proof state before:
α : Type
a : α
⊢ ¬LEMCounterexampleModel ⊧ atom a ⋎ ~atom a
Tactic:
simp [ValidOnModel.iff_models, Satisfies.iff_models, ValidOnModel, Satisfies, LEMCounterexampleModel]
Proof state after:
α : Type
a : α
⊢ ∃ x, ¬x = 1 ∧ x ≺ 1
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_atom
Proof state before:
α : Type
a : α
⊢ ∃ x, ¬x = 1 ∧ x ≺ 1
Tactic:
use 0
Proof state after:
case h
α : Type
a : α
⊢ ¬0 = 1 ∧ 0 ≺ 1
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_atom
Proof state before:
case h
α : Type
a : α
⊢ ¬0 = 1 ∧ 0 ≺ 1
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
Tactic:
simp [ValidOnFrameClass.iff_models, ValidOnFrameClass]
Proof state after:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ∃ x ∈ 𝔽(𝗘𝗙𝗤), ¬ValidOnFrame x (p ⋎ (p ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ∃ x ∈ 𝔽(𝗘𝗙𝗤), ¬ValidOnFrame x (p ⋎ (p ⟶ ⊥))
Tactic:
existsi (atom default), (LEMCounterexampleModel).Frame
Proof state after:
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)

case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)

case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
. apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr;
  trivial;
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
. simp [ValidOnFrame];
  existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary;
  apply noLEM_atom;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)
Tactic:
apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr
Proof state after:
case left
α : Type
inst✝ : Inhabited α
⊢ True
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case left
α : Type
inst✝ : Inhabited α
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
simp [ValidOnFrame]
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ x,
    ∃ (x_1 : ∀ {w₁ w₂ : LEMCounterexampleModel.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ¬ValidOnModel { Frame := LEMCounterexampleModel.Frame, Valuation := x, hereditary := x_1 }
          (atom default ⋎ (atom default ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ x,
    ∃ (x_1 : ∀ {w₁ w₂ : LEMCounterexampleModel.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ¬ValidOnModel { Frame := LEMCounterexampleModel.Frame, Valuation := x, hereditary := x_1 }
          (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_on_frameclass
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
apply noLEM_atom
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM
Proof state before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
obtain ⟨p, _⟩ : ∃ (p : Formula α), ¬(𝔽(Ax(𝐈𝐧𝐭))) ⊧ p ⋎ ~p := noLEM_on_frameclass
Proof state after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM
Proof state before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
existsi p
Proof state after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM
Proof state before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
by_contra hC
Proof state after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM
Proof state before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
⊢ False
Tactic:
have : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p := sound! hC
Proof state after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
this : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM
Proof state before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
this : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 <ₛ 𝐂𝐥
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Tactic:
. exact reducible_efq_dne;
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case left
α : Type
inst✝ : Inhabited α
⊢ 𝐈𝐧𝐭 ≤ₛ 𝐂𝐥
Tactic:
exact reducible_efq_dne
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ≤ₛ 𝐈𝐧𝐭
Tactic:
apply reducible_iff.not.mpr
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬∀ {f : Formula α}, 𝐂𝐥 ⊢! f → 𝐈𝐧𝐭 ⊢! f
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬∀ {f : Formula α}, 𝐂𝐥 ⊢! f → 𝐈𝐧𝐭 ⊢! f
Tactic:
push_neg
Proof state after:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Tactic:
obtain ⟨p, hp⟩ := noLEM (α := α)
Proof state after:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ∃ f, 𝐂𝐥 ⊢! f ∧ ¬𝐈𝐧𝐭 ⊢! f
Tactic:
existsi (p ⋎ ~p)
Proof state after:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p ∧ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right.intro
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p ∧ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
constructor
Proof 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
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof 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!;
Proof state after:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
. assumption;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right.intro.left
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ 𝐂𝐥 ⊢! p ⋎ ~p
Tactic:
exact lem!
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.strictReducible_intuitionistic_classical
Proof state before:
case right.intro.right
α : Type
inst✝ : Inhabited α
p : Formula α
hp : 𝐈𝐧𝐭 ⊬! p ⋎ ~p
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ ~p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.translationAux_neg
Proof state before:
L L' : Language
inst✝ : L.Eq
T : Theory L
ι : Interpretation T L'
n : ℕ
p : Semisentence L' n
⊢ ι.translationAux (~p) = ~ι.translationAux p
Tactic:
induction p using Semiformula.rec' <;> simp [translationAux, *, ←Semiformula.neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.sub_exists
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
⊢ ∃ x, ι.Dom x
Tactic:
simpa [Dom, models_iff, eval_substs, Matrix.constant_eq_singleton] using consequence_iff_add_eq.mp ι.domain_nonempty M inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.func_existsUnique_on_dom
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
⊢ ∀ (v : Fin k → M), (∀ (i : Fin k), ι.Dom (v i)) → ∃! y, ι.Dom y ∧ (Evalbm M (y :> v)) (ι.func f)
Tactic:
simpa [Dom, models_iff, eval_substs, Matrix.constant_eq_singleton] using consequence_iff_add_eq.mp (ι.func_defined f) M inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
have : ∃! y, ι.Dom y ∧ Evalbm M (y :> fun i ↦ v i) (ι.func f) := ι.func_existsUnique_on_dom M f (fun i ↦ v i) (fun i ↦ by simp [(v i).prop])
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
rcases this.exists with ⟨y, hy, Hy⟩
Proof state after:
case intro.intro
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
case intro.intro
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
exact ExistsUnique.intro ⟨y, hy⟩ (by simpa using Hy) (by simp; intro z hz Hz; exact this.unique ⟨hz, Hz⟩ ⟨hy, Hy⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
i : Fin k
⊢ ι.Dom ((fun i => ↑(v i)) i)
Tactic:
simp [(v i).prop]
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ (Evalbm M (↑⟨y, hy⟩ :> fun i => ↑(v i))) (ι.func f)
Tactic:
simpa using Hy
Proof state after:
no goals