internlm/Lean-Github huggingface dataset:
Theorem: append_assoc'
Proof state before:
α : Type
as bs cs : List α
a b c : α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)
Tactic:
induction as with
| nil => rw [nil_append, nil_append]
| cons a as ih => rw [cons_append, cons_append, ih, cons_append]
Proof state after:
no goals
Theorem: append_assoc'
Proof state before:
case nil
α : Type
as bs cs : List α
a b c : α
⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)
Tactic:
rw [nil_append, nil_append]
Proof state after:
no goals
Theorem: append_assoc'
Proof state before:
case cons
α : Type
as✝ bs cs : List α
a✝ b c a : α
as : List α
ih : as ++ bs ++ cs = as ++ (bs ++ cs)
⊢ a :: as ++ bs ++ cs = a :: as ++ (bs ++ cs)
Tactic:
rw [cons_append, cons_append, ih, cons_append]
Proof state after:
no goals
Theorem: reverseAux_append
Proof state before:
α : Type
as bs cs : List α
a b c : α
⊢ reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs)
Tactic:
induction as generalizing cs with
| nil => rw [nil_append, reverseAux]
| cons a as ih => rw [cons_append, reverseAux, reverseAux, ih]
Proof state after:
no goals
Theorem: reverseAux_append
Proof state before:
case nil
α : Type
bs : List α
a b c : α
cs : List α
⊢ reverseAux ([] ++ bs) cs = reverseAux bs (reverseAux [] cs)
Tactic:
rw [nil_append, reverseAux]
Proof state after:
no goals
Theorem: reverseAux_append
Proof state before:
case cons
α : Type
bs : List α
a✝ b c a : α
as : List α
ih : ∀ (cs : List α), reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs)
cs : List α
⊢ reverseAux (a :: as ++ bs) cs = reverseAux bs (reverseAux (a :: as) cs)
Tactic:
rw [cons_append, reverseAux, reverseAux, ih]
Proof state after:
no goals
Theorem: reverseAux_append'
Proof state before:
α : Type
as bs cs : List α
a b c : α
⊢ reverseAux as (bs ++ cs) = reverseAux as bs ++ cs
Tactic:
induction as generalizing bs with
| nil => rw [reverseAux, reverseAux]
| cons a as ih => rw [reverseAux, reverseAux, ←cons_append, ih]
Proof state after:
no goals
Theorem: reverseAux_append'
Proof state before:
case nil
α : Type
cs : List α
a b c : α
bs : List α
⊢ reverseAux [] (bs ++ cs) = reverseAux [] bs ++ cs
Tactic:
rw [reverseAux, reverseAux]
Proof state after:
no goals
Theorem: reverseAux_append'
Proof state before:
case cons
α : Type
cs : List α
a✝ b c a : α
as : List α
ih : ∀ (bs : List α), reverseAux as (bs ++ cs) = reverseAux as bs ++ cs
bs : List α
⊢ reverseAux (a :: as) (bs ++ cs) = reverseAux (a :: as) bs ++ cs
Tactic:
rw [reverseAux, reverseAux, ←cons_append, ih]
Proof state after:
no goals
Theorem: reverse_append
Proof state before:
α : Type
as bs cs : List α
a b c : α
⊢ reverse (as ++ bs) = reverse bs ++ reverse as
Tactic:
rw [reverse, reverseAux_append, reverse, ←reverseAux_append', nil_append,
    reverse]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
h : ¬Occurs v A
b : Bool
⊢ eval (fun w => if v = w then b else τ w) A = eval τ A
Tactic:
induction A with
| var s =>
  rw [eval]
  rw [Occurs] at h
  rw [if_neg h, eval]
| tr =>
  rw [eval, eval]
| fls =>
  rw [eval, eval]
| neg A ihA =>
  rw [eval, eval]
  rw [Occurs] at h
  rw [ihA h]
| conj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| disj A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| impl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
| biImpl A B ihA ihB =>
  rw [Occurs, not_or] at h
  rcases h with ⟨hA, hB⟩
  rw [eval, eval, ihA hA, ihB hB]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ eval (fun w => if v = w then b else τ w) (var s) = eval τ (var s)
Tactic:
rw [eval]
Proof state after:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ (if v = s then b else τ s) = eval τ (var s)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬Occurs v (var s)
⊢ (if v = s then b else τ s) = eval τ (var s)
Tactic:
rw [Occurs] at h
Proof state after:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬v = s
⊢ (if v = s then b else τ s) = eval τ (var s)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case var
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
s : String
h : ¬v = s
⊢ (if v = s then b else τ s) = eval τ (var s)
Tactic:
rw [if_neg h, eval]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case tr
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
h : ¬Occurs v tr
⊢ eval (fun w => if v = w then b else τ w) tr = eval τ tr
Tactic:
rw [eval, eval]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case fls
α : Type
as bs cs : List α
a b✝ c : α
A B : PropForm
τ : String → Bool
v : String
b : Bool
h : ¬Occurs v fls
⊢ eval (fun w => if v = w then b else τ w) fls = eval τ fls
Tactic:
rw [eval, eval]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ eval (fun w => if v = w then b else τ w) (neg A) = eval τ (neg A)
Tactic:
rw [eval, eval]
Proof state after:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v (neg A)
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Tactic:
rw [Occurs] at h
Proof state after:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v A
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case neg
α : Type
as bs cs : List α
a b✝ c : α
A✝ B : PropForm
τ : String → Bool
v : String
b : Bool
A : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
h : ¬Occurs v A
⊢ (!eval (fun w => if v = w then b else τ w) A) = !eval τ A
Tactic:
rw [ihA h]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (conj A B)
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rw [Occurs, not_or] at h
Proof state after:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case conj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rcases h with ⟨hA, hB⟩
Proof state after:
case conj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case conj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (conj A B) = eval τ (conj A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (disj A B)
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rw [Occurs, not_or] at h
Proof state after:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case disj
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rcases h with ⟨hA, hB⟩
Proof state after:
case disj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case disj.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (disj A B) = eval τ (disj A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (impl A B)
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rw [Occurs, not_or] at h
Proof state after:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case impl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rcases h with ⟨hA, hB⟩
Proof state after:
case impl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case impl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (impl A B) = eval τ (impl A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
Proof state after:
no goals
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v (biImpl A B)
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rw [Occurs, not_or] at h
Proof state after:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case biImpl
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
h : ¬Occurs v A ∧ ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rcases h with ⟨hA, hB⟩
Proof state after:
case biImpl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Theorem: PropForm.eval_of_not_occurs
Proof state before:
case biImpl.intro
α : Type
as bs cs : List α
a b✝ c : α
A✝ B✝ : PropForm
τ : String → Bool
v : String
b : Bool
A B : PropForm
ihA : ¬Occurs v A → eval (fun w => if v = w then b else τ w) A = eval τ A
ihB : ¬Occurs v B → eval (fun w => if v = w then b else τ w) B = eval τ B
hA : ¬Occurs v A
hB : ¬Occurs v B
⊢ eval (fun w => if v = w then b else τ w) (biImpl A B) = eval τ (biImpl A B)
Tactic:
rw [eval, eval, ihA hA, ihB hB]
Proof state after:
no goals
Theorem: dpllSatYesSpec
Proof state before:
⊢ ∀ (ϕ : CnfForm) (τ : PropAssignment), dpllSat ϕ = some τ ↔ PropAssignment.evalCnf τ ϕ = true
Tactic:
admit
Proof state after:
no goals
Theorem: dpllSatNoSpec
Proof state before:
⊢ ∀ (ϕ : CnfForm), dpllSat ϕ = none ↔ ∀ (τ : PropAssignment), PropAssignment.evalCnf τ ϕ = false
Tactic:
admit
Proof state after:
no goals
Theorem: and_swap'
Proof state before:
P Q R : Prop
⊢ P ∧ Q → Q ∧ P
Tactic:
intro h
Proof state after:
P Q R : Prop
h : P ∧ Q
⊢ Q ∧ P
Theorem: and_swap'
Proof state before:
P Q R : Prop
h : P ∧ Q
⊢ Q ∧ P
Tactic:
rcases h with ⟨h1, h2⟩
Proof state after:
case intro
P Q R : Prop
h1 : P
h2 : Q
⊢ Q ∧ P
Theorem: and_swap'
Proof state before:
case intro
P Q R : Prop
h1 : P
h2 : Q
⊢ Q ∧ P
Tactic:
constructor
Proof state after:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q

case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Theorem: and_swap'
Proof state before:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q

case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
. exact h2
Proof state after:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Theorem: and_swap'
Proof state before:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
. exact h1
Proof state after:
no goals
Theorem: and_swap'
Proof state before:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q
Tactic:
exact h2
Proof state after:
no goals
Theorem: and_swap'
Proof state before:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: or_swap'
Proof state before:
P Q R : Prop
⊢ P ∨ Q → Q ∨ P
Tactic:
intro h
Proof state after:
P Q R : Prop
h : P ∨ Q
⊢ Q ∨ P
Theorem: or_swap'
Proof state before:
P Q R : Prop
h : P ∨ Q
⊢ Q ∨ P
Tactic:
rcases h with h1 |  h2
Proof state after:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P

case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Theorem: or_swap'
Proof state before:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P

case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
. right; exact h1
Proof state after:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Theorem: or_swap'
Proof state before:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
. left; exact h2
Proof state after:
no goals
Theorem: or_swap'
Proof state before:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P
Tactic:
right
Proof state after:
case inl.h
P Q R : Prop
h1 : P
⊢ P
Theorem: or_swap'
Proof state before:
case inl.h
P Q R : Prop
h1 : P
⊢ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: or_swap'
Proof state before:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
left
Proof state after:
case inr.h
P Q R : Prop
h2 : Q
⊢ Q
Theorem: or_swap'
Proof state before:
case inr.h
P Q R : Prop
h2 : Q
⊢ Q
Tactic:
exact h2
Proof state after:
no goals
Theorem: Function.Graph.iff_left
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
f : α → σ
y : σ
x : α
⊢ f x = y ↔ Graph f y x
Tactic:
simp [Graph, eq_comm]
Proof state after:
no goals
Theorem: Function.Graph.iff_right
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
f : α → σ
y : σ
x : α
⊢ y = f x ↔ Graph f y x
Tactic:
simp [Graph]
Proof state after:
no goals
Theorem: Function.Graph₂.iff_left
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
f : α → β → σ
y : σ
x₁ : α
x₂ : β
⊢ f x₁ x₂ = y ↔ Graph₂ f y x₁ x₂
Tactic:
simp [Graph₂, eq_comm]
Proof state after:
no goals
Theorem: Function.Graph₂.iff_right
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
f : α → β → σ
y : σ
x₁ : α
x₂ : β
⊢ y = f x₁ x₂ ↔ Graph₂ f y x₁ x₂
Tactic:
simp [Graph₂]
Proof state after:
no goals
Theorem: Function.Graph₃.iff_left
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
γ : Sort u_4
f : α → β → γ → σ
y : σ
x₁ : α
x₂ : β
x₃ : γ
⊢ f x₁ x₂ x₃ = y ↔ Graph₃ f y x₁ x₂ x₃
Tactic:
simp [Graph₃, eq_comm]
Proof state after:
no goals
Theorem: Function.Graph₃.iff_right
Proof state before:
σ : Sort u_1
α : Sort u_2
β : Sort u_3
γ : Sort u_4
f : α → β → γ → σ
y : σ
x₁ : α
x₂ : β
x₃ : γ
⊢ y = f x₁ x₂ x₃ ↔ Graph₃ f y x₁ x₂ x₃
Tactic:
simp [Graph₃]
Proof state after:
no goals
Theorem: Matrix.forall_iff
Proof state before:
α : Type u_1
n : ℕ
p : (Fin (n + 1) → α) → Prop
h : ∀ (a : α) (v : Fin n → α), p (a :> v)
v : Fin (n + 1) → α
⊢ p v
Tactic:
simpa [←eq_vecCons v] using h (v 0) (v ∘ Fin.succ)
Proof state after:
no goals
Theorem: Set.subset_union_three₁
Proof state before:
α : Type u_1
s t u : Set α
⊢ s ⊆ s ∪ t
Tactic:
simp
Proof state after:
no goals
Theorem: Set.subset_union_three₂
Proof state before:
α : Type u_1
s t u : Set α
⊢ t ⊆ s ∪ t
Tactic:
simp
Proof state after:
no goals
Theorem: Set.subset_union_three₃
Proof state before:
α : Type u_1
s t u : Set α
⊢ u ⊆ u
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.fun_eq_vec₃
Proof state before:
α : Type u_1
v : Fin 3 → α
⊢ v = ![v 0, v 1, v 2]
Tactic:
funext x
Proof state after:
case h
α : Type u_1
v : Fin 3 → α
x : Fin 3
⊢ v x = ![v 0, v 1, v 2] x
Theorem: Matrix.fun_eq_vec₃
Proof state before:
case h
α : Type u_1
v : Fin 3 → α
x : Fin 3
⊢ v x = ![v 0, v 1, v 2] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
Proof state after:
case h.succ
α : Type u_1
v : Fin 3 → α
x : Fin 2
⊢ v x.succ = ![v 1, v 2] x
Theorem: Matrix.fun_eq_vec₃
Proof state before:
case h.succ
α : Type u_1
v : Fin 3 → α
x : Fin 2
⊢ v x.succ = ![v 1, v 2] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: Matrix.fun_eq_vec₄
Proof state before:
α : Type u_1
v : Fin 4 → α
⊢ v = ![v 0, v 1, v 2, v 3]
Tactic:
funext x
Proof state after:
case h
α : Type u_1
v : Fin 4 → α
x : Fin 4
⊢ v x = ![v 0, v 1, v 2, v 3] x
Theorem: Matrix.fun_eq_vec₄
Proof state before:
case h
α : Type u_1
v : Fin 4 → α
x : Fin 4
⊢ v x = ![v 0, v 1, v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
Proof state after:
case h.succ
α : Type u_1
v : Fin 4 → α
x : Fin 3
⊢ v x.succ = ![v 1, v 2, v 3] x
Theorem: Matrix.fun_eq_vec₄
Proof state before:
case h.succ
α : Type u_1
v : Fin 4 → α
x : Fin 3
⊢ v x.succ = ![v 1, v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
Proof state after:
case h.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 2
⊢ v x.succ.succ = ![v 2, v 3] x
Theorem: Matrix.fun_eq_vec₄
Proof state before:
case h.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 2
⊢ v x.succ.succ = ![v 2, v 3] x
Tactic:
cases' x using Fin.cases with x <;> simp [Fin.eq_zero]
Proof state after:
case h.succ.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 1
⊢ v (Fin.succ 2) = v 3
Theorem: Matrix.fun_eq_vec₄
Proof state before:
case h.succ.succ.succ
α : Type u_1
v : Fin 4 → α
x : Fin 1
⊢ v (Fin.succ 2) = v 3
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.eq_vecCons'
Proof state before:
n : ℕ
C : Type u_1
s : Fin (n + 1) → C
⊢ (s 0 :> fun x => s x.succ) 0 = s 0
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.eq_vecCons'
Proof state before:
n : ℕ
C : Type u_1
s : Fin (n + 1) → C
⊢ ∀ (i : Fin n), (s 0 :> fun x => s x.succ) i.succ = s i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: LO.SigmaPiDelta.alt_coe
Proof state before:
Γ : Polarity
⊢ Γ.coe.alt = Γ.alt.coe
Tactic:
cases Γ <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin n → Semiformula L ξ 1
q : Semiformula L ξ n
⊢ (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Tactic:
induction' n with n IH
Proof state after:
case zero
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin 0 → Semiformula L ξ 1
q : Semiformula L ξ 0
⊢ (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin 0 → M), (∀ (i : Fin 0), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q

case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (Evalf s ε) (ballClosure p q) ↔
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q