internlm/Lean-Github huggingface dataset:
Theorem: List.isEmpty_reverse
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ decide (l.reverse = []) = decide (l = [])
Tactic:
simp only [reverse_eq_nil_iff]
Proof state after:
no goals
Theorem: List.reverse_dropLast
Proof state before:
C : Type u_1
α : Type u_2
l✝ l : List α
x head✝ : α
tail✝ : List α
⊢ (x :: head✝ :: tail✝).dropLast.reverse = (x :: head✝ :: tail✝).reverse.tail
Tactic:
rw [dropLast, reverse_cons x, reverse_cons x, reverse_dropLast (_::_),
  tail_append_of_ne_nil] <;> simp
Proof state after:
no goals
Theorem: List.back?_toArray
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ (toArray l).back? = l.getLast?
Tactic:
rw [Array.back?, Array.get?_eq_data_get?, getLast?_eq_get?]
Proof state after:
C : Type u_1
α : Type u_2
l : List α
⊢ (toArray l).data.get? ((toArray l).size - 1) = l.get? (l.length - 1)
Theorem: List.back?_toArray
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ (toArray l).data.get? ((toArray l).size - 1) = l.get? (l.length - 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Array.isEmpty_data
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.data.isEmpty = a.isEmpty
Tactic:
rw [List.isEmpty_eq_decide_length, isEmpty]
Proof state after:
no goals
Theorem: Array.isEmpty_toList
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.isEmpty = a.isEmpty
Tactic:
rw [isEmpty_data, toList_eq]
Proof state after:
no goals
Theorem: Array.isEmpty_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toListRev.isEmpty = a.isEmpty
Tactic:
rw [toListRev_eq, List.isEmpty_reverse, isEmpty_data]
Proof state after:
no goals
Theorem: Array.toList_length
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.length = a.size
Tactic:
rw [toList_eq, data_length]
Proof state after:
no goals
Theorem: Array.get?_data
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.data.get? = a.get?
Tactic:
ext i
Proof state after:
case h.a
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
a✝ : α
⊢ a✝ ∈ a.data.get? i ↔ a✝ ∈ a.get? i
Theorem: Array.get?_data
Proof state before:
case h.a
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
a✝ : α
⊢ a✝ ∈ a.data.get? i ↔ a✝ ∈ a.get? i
Tactic:
rw [Array.get?_eq_data_get?]
Proof state after:
no goals
Theorem: Array.get?_toList
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.get? = a.get?
Tactic:
rw [toList_eq, get?_data]
Proof state after:
no goals
Theorem: Array.get?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
h : i < a.size
⊢ a.toListRev.get? i = a.get? (a.size - 1 - i)
Tactic:
rw [toListRev_eq, List.get?_reverse _ (by rwa [data_length]), get?_data]
Proof state after:
no goals
Theorem: Array.get?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
h : i < a.size
⊢ i < a.data.length
Tactic:
rwa [data_length]
Proof state after:
no goals
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toListRev.head? = a.back?
Tactic:
cases a.size.eq_zero_or_pos
Proof state after:
case inl
C : Type u_1
α : Type u_2
a : Array α
h✝ : a.size = 0
⊢ a.toListRev.head? = a.back?

case inr
C : Type u_1
α : Type u_2
a : Array α
h✝ : a.size > 0
⊢ a.toListRev.head? = a.back?
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.toListRev.head? = a.back?
Tactic:
case inl h =>
  rw [toListRev_eq, back?, ← get?_data]
  simp [List.length_eq_zero.mp h]
Proof state after:
no goals
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.toListRev.head? = a.back?
Tactic:
case inr h =>
  rw [← List.get?_zero, get?_toListRev _ _ h, Nat.sub_zero]
  rfl
Proof state after:
no goals
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.toListRev.head? = a.back?
Tactic:
rw [toListRev_eq, back?, ← get?_data]
Proof state after:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.data.reverse.head? = a.data.get? (a.size - 1)
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size = 0
⊢ a.data.reverse.head? = a.data.get? (a.size - 1)
Tactic:
simp [List.length_eq_zero.mp h]
Proof state after:
no goals
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.toListRev.head? = a.back?
Tactic:
rw [← List.get?_zero, get?_toListRev _ _ h, Nat.sub_zero]
Proof state after:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.get? (a.size - 1) = a.back?
Theorem: Array.head?_toListRev
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
h : a.size > 0
⊢ a.get? (a.size - 1) = a.back?
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.getLast?_toList
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.getLast? = a.back?
Tactic:
rw [back?, get?_eq_data_get?, List.getLast?_eq_get?]
Proof state after:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.get? (a.toList.length - 1) = a.data.get? (a.size - 1)
Theorem: Array.getLast?_toList
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.get? (a.toList.length - 1) = a.data.get? (a.size - 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Array.getLast?_data
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.data.getLast? = a.back?
Tactic:
simp [← getLast?_toList]
Proof state after:
no goals
Theorem: Array.dropLast_toList
Proof state before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.toList.dropLast = a.pop.toList
Tactic:
simp
Proof state after:
no goals
Theorem: ToList.lawfulEmptyCollection_iff
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ LawfulEmptyCollection C α ↔ toList ∅ = []
Tactic:
rw [ToMultiset.lawfulEmptyCollection_iff]
Proof state after:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toList ∅ = []
Theorem: ToList.lawfulEmptyCollection_iff
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toList ∅ = []
Tactic:
simp [toMultiset]
Proof state after:
no goals
Theorem: toList_empty
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
inst : LawfulEmptyCollection C α
⊢ toList ∅ = []
Tactic:
rwa [ToList.lawfulEmptyCollection_iff] at inst
Proof state after:
no goals
Theorem: size_eq_size_toArray
Proof state before:
C : Type u_1
α : Type u_2
inst✝ : ToList C α
c : C
⊢ size c = (toArray c).size
Tactic:
simp [size_eq_length_toList]
Proof state after:
no goals
Theorem: isEmpty_toList
Proof state before:
C : Type u_1
α : Type u_2
inst✝ : ToList C α
c : C
⊢ (toList c).isEmpty = isEmpty c
Tactic:
rw [isEmpty_eq_decide_size, List.isEmpty_eq_decide_length, size_eq_length_toList]
Proof state after:
no goals
Theorem: front?_isSome
Proof state before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : Front C α
c : C
h : ¬isEmpty c = true
⊢ (front? c).isSome = true
Tactic:
rwa [front?_def, List.head?_isSome, ← List.not_isEmpty_iff_ne_nil, isEmpty_toList]
Proof state after:
no goals
Theorem: front_def
Proof state before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : Front C α
c : C
h : ¬isEmpty c = true
⊢ some (front c h) = some ((front? c).get ⋯)
Tactic:
simpa using (front_mem c h).symm
Proof state after:
no goals
Theorem: back?_isSome
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : Back C α
c : C
h : ¬isEmpty c = true
⊢ (back? c).isSome = true
Tactic:
rwa [back?_def, List.getLast?_isSome, ← List.not_isEmpty_iff_ne_nil, isEmpty_toList]
Proof state after:
no goals
Theorem: back_def
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : Back C α
c : C
h : ¬isEmpty c = true
⊢ some (back c h) = some ((back? c).get ⋯)
Tactic:
simpa using (back_mem c h).symm
Proof state after:
no goals
Theorem: ToList.RandomAccess.get_toArray
Proof state before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = get c (Fin.cast ⋯ i)
Tactic:
rw [get_eq_get_toArray]
Proof state after:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = (toArray c).get (Fin.cast ⋯ (Fin.cast ⋯ i))
Theorem: ToList.RandomAccess.get_toArray
Proof state before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : RandomAccess C α
c : C
i : Fin (toArray c).size
⊢ (toArray c).get i = (toArray c).get (Fin.cast ⋯ (Fin.cast ⋯ i))
Tactic:
rfl
Proof state after:
no goals
Theorem: ToFinset.lawfulEmptyCollection_iff
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
⊢ LawfulEmptyCollection C α ↔ toFinset ∅ = ∅
Tactic:
rw [ToMultiset.lawfulEmptyCollection_iff]
Proof state after:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toFinset ∅ = ∅
Theorem: ToFinset.lawfulEmptyCollection_iff
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
⊢ ToMultiset.toMultiset ∅ = 0 ↔ toFinset ∅ = ∅
Tactic:
change (toFinset (∅ : C)).val = ∅ ↔ _
Proof state after:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
⊢ (toFinset ∅).val = ∅ ↔ toFinset ∅ = ∅
Theorem: ToFinset.lawfulEmptyCollection_iff
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
⊢ (toFinset ∅).val = ∅ ↔ toFinset ∅ = ∅
Tactic:
simp
Proof state after:
no goals
Theorem: toFinset_empty
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝⁴ : ToFinset C α
c : C
inst✝³ : EmptyCollection C
inst✝² : LawfulEmptyCollection C α
inst✝¹ : ToFinset C α
inst✝ : EmptyCollection C
inst : LawfulEmptyCollection C α
⊢ toFinset ∅ = ∅
Tactic:
rwa [ToFinset.lawfulEmptyCollection_iff] at inst
Proof state after:
no goals
Theorem: Forest.roots_subset_support
Proof state before:
α : Type u_1
f : Forest α
⊢ f.roots ⊆ f.support
Tactic:
induction f with
| nil => rfl
| node a c s _ ihs =>
  exact Set.insert_subset_insert (Set.subset_union_of_subset_right ihs _)
Proof state after:
no goals
Theorem: Forest.roots_subset_support
Proof state before:
case nil
α : Type u_1
⊢ nil.roots ⊆ nil.support
Tactic:
rfl
Proof state after:
no goals
Theorem: Forest.roots_subset_support
Proof state before:
case node
α : Type u_1
a : α
c s : Forest α
child_ih✝ : c.roots ⊆ c.support
ihs : s.roots ⊆ s.support
⊢ (node a c s).roots ⊆ (node a c s).support
Tactic:
exact Set.insert_subset_insert (Set.subset_union_of_subset_right ihs _)
Proof state after:
no goals
Theorem: toMultiset_of_isEmpty
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝ : ToMultiset C α
c : C
h : isEmpty c = true
⊢ toMultiset c = 0
Tactic:
simpa [size_eq_card_toMultiset] using h
Proof state after:
no goals
Theorem: ToMultiset.not_isEmpty_of_mem
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝ : ToMultiset C α
c✝ c : C
v : α
hv : v ∈ c
⊢ ¬isEmpty c = true
Tactic:
simpa [size_eq_card_toMultiset, Multiset.eq_zero_iff_forall_not_mem] using ⟨v, hv⟩
Proof state after:
no goals
Theorem: count_toMultiset_ne_zero
Proof state before:
α✝ : Type u_1
C : Type u_2
α : Type u_3
inst✝¹ : ToMultiset C α
c✝ : C
inst✝ : DecidableEq α
a : α
c : C
⊢ Multiset.count a (toMultiset c) ≠ 0 ↔ a ∈ c
Tactic:
simp [count_toMultiset_eq_zero, mem_toMultiset]
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.insertEmpty
Proof state before:
L✝ : Type u
inst✝³ : DecidableEq L✝
inst✝² : HasMinimalLogicSymbols L✝
L : Type u
inst✝¹ : DecidableEq L
inst✝ : HilbertSystem L
ψ φ : L
⊢ ({φ} ⊢ ψ) → (∅ ∪ {φ} ⊢ ψ)
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.weakenImp
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Finset L
ψ φ : L
⊢ (Γ ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
exact λ h => MP (axiomK _ ψ φ) h
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.weakenContext
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
Γ Δ : Context L
hs : Γ ⊆ Δ
⊢ (Γ ⊢ φ) → (Δ ⊢ φ)
Tactic:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.weakenContext'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
Γ : Context L
⊢ ∅ ⊆ Γ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
⊢ ∅ ⊢ φ →' φ
Tactic:
have s1 : ⊢ (φ →' (φ →' φ) →' φ) := by apply axiomK;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
⊢ ∅ ⊢ φ →' φ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s2 : ⊢ ((φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ) := by apply axiomS;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s3 : ⊢ ((φ →' φ →' φ) →' φ →' φ) := MP s2 s1
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s4 : ⊢ (φ →' φ →' φ) := by apply axiomK;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
s4 : ∅ ⊢ φ →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
s4 : ∅ ⊢ φ →' φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
have s5 : ⊢ (φ →' φ) := MP s3 s4
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
s4 : ∅ ⊢ φ →' φ →' φ
s5 : ∅ ⊢ φ →' φ
⊢ ∅ ⊢ φ →' φ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
s4 : ∅ ⊢ φ →' φ →' φ
s5 : ∅ ⊢ φ →' φ
⊢ ∅ ⊢ φ →' φ
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
⊢ ∅ ⊢ φ →' (φ →' φ) →' φ
Tactic:
apply axiomK
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
⊢ ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
Tactic:
apply axiomS
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id_imp'
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
s1 : ∅ ⊢ φ →' (φ →' φ) →' φ
s2 : ∅ ⊢ (φ →' (φ →' φ) →' φ) →' (φ →' φ →' φ) →' φ →' φ
s3 : ∅ ⊢ (φ →' φ →' φ) →' φ →' φ
⊢ ∅ ⊢ φ →' φ →' φ
Tactic:
apply axiomK
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.id
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
φ : L
⊢ φ ∈ {φ}
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) ↔ (Γ ∪ {φ} ⊢ ψ)
Tactic:
apply Iff.intro
Proof state after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)

case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)

case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
. intro h;
  have h1 : (Γ ∪ {φ}) ⊢ (φ →' ψ) := weakenContext Γ (Γ ∪ {φ}) (subset_union_left _ _) h;
  have h2 := context (Γ ∪ {φ}) φ (by simp);
  exact MP h1 h2;
Proof state after:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
. admit
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ⊢ φ →' ψ) → (Γ ∪ {φ} ⊢ ψ)
Tactic:
intro h
Proof state after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
have h1 : (Γ ∪ {φ}) ⊢ (φ →' ψ) := weakenContext Γ (Γ ∪ {φ}) (subset_union_left _ _) h
Proof state after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
have h2 := context (Γ ∪ {φ}) φ (by simp)
Proof state after:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
h2 : Γ ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ} ⊢ ψ
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mp
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
h2 : Γ ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ} ⊢ ψ
Tactic:
exact MP h1 h2
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
h : Γ ⊢ φ →' ψ
h1 : Γ ∪ {φ} ⊢ φ →' ψ
⊢ φ ∈ Γ ∪ {φ}
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.deduction
Proof state before:
case mpr
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ : L
⊢ (Γ ∪ {φ} ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
admit
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ φ →' ¬'¬'φ
Tactic:
simp [deduction]
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Tactic:
have s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥' := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
s2 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥'
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'