internlm/Lean-Github huggingface dataset:
Theorem: LoVe.map_comp
Proof state before:
case cons
α β γ : Type
f : α → β
g : β → γ
x : α
xs' : List α
ih : map g (map f xs') = map (fun x => g (f x)) xs'
⊢ map g (map f (x :: xs')) = map (fun x => g (f x)) (x :: xs')
Tactic:
simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.map_append
Proof state before:
α β : Type
f : α → β
xs ys : List α
⊢ map f (xs ++ ys) = map f xs ++ map f ys
Tactic:
induction xs with
| nil           => rfl
| cons x xs' ih => simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.map_append
Proof state before:
case nil
α β : Type
f : α → β
ys : List α
⊢ map f ([] ++ ys) = map f [] ++ map f ys
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.map_append
Proof state before:
case cons
α β : Type
f : α → β
ys : List α
x : α
xs' : List α
ih : map f (xs' ++ ys) = map f xs' ++ map f ys
⊢ map f (x :: xs' ++ ys) = map f (x :: xs') ++ map f ys
Tactic:
simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.min_add_add
Proof state before:
l m n : ℕ
⊢ min (m + l) (n + l) = min m n + l
Tactic:
cases Classical.em (m ≤ n) with
| inl h => simp [min, h]
| inr h => simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add
Proof state before:
case inl
l m n : ℕ
h : m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add
Proof state before:
case inr
l m n : ℕ
h : ¬m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add_match
Proof state before:
l m n : ℕ
h : m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add_match
Proof state before:
l m n : ℕ
h : ¬m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add_if
Proof state before:
l m n : ℕ
h : m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.min_add_add_if
Proof state before:
l m n : ℕ
h : ¬m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
Proof state after:
no goals
Theorem: LoVe.length_zip
Proof state before:
α β : Type
xs : List α
ys : List β
⊢ length (zip xs ys) = min (length xs) (length ys)
Tactic:
induction xs generalizing ys with
| nil           => simp [min, length]
| cons x xs' ih =>
  cases ys with
  | nil        => rfl
  | cons y ys' => simp [zip, length, ih ys', min_add_add]
Proof state after:
no goals
Theorem: LoVe.length_zip
Proof state before:
case nil
α β : Type
ys : List β
⊢ length (zip [] ys) = min (length []) (length ys)
Tactic:
simp [min, length]
Proof state after:
no goals
Theorem: LoVe.length_zip
Proof state before:
case cons
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
ys : List β
⊢ length (zip (x :: xs') ys) = min (length (x :: xs')) (length ys)
Tactic:
cases ys with
| nil        => rfl
| cons y ys' => simp [zip, length, ih ys', min_add_add]
Proof state after:
no goals
Theorem: LoVe.length_zip
Proof state before:
case cons.nil
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
⊢ length (zip (x :: xs') []) = min (length (x :: xs')) (length [])
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.length_zip
Proof state before:
case cons.cons
α β : Type
x : α
xs' : List α
ih : ∀ (ys : List β), length (zip xs' ys) = min (length xs') (length ys)
y : β
ys' : List β
⊢ length (zip (x :: xs') (y :: ys')) = min (length (x :: xs')) (length (y :: ys'))
Tactic:
simp [zip, length, ih ys', min_add_add]
Proof state after:
no goals
Theorem: LoVe.map_zip
Proof state before:
α α' β β' : Type
f : α → α'
g : β → β'
x : α
xs : List α
y : β
ys : List β
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip (x :: xs) (y :: ys)) = zip (map f (x :: xs)) (map g (y :: ys))
Tactic:
simp [zip, map, map_zip f g xs ys]
Proof state after:
no goals
Theorem: LoVe.map_zip
Proof state before:
α α' β β' : Type
f : α → α'
g : β → β'
x✝ : List β
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip [] x✝) = zip (map f []) (map g x✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.map_zip
Proof state before:
α α' β β' : Type
f : α → α'
g : β → β'
head✝ : α
tail✝ : List α
⊢ map (fun ab => (f ab.fst, g ab.snd)) (zip (head✝ :: tail✝) []) = zip (map f (head✝ :: tail✝)) (map g [])
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mirror_mirror
Proof state before:
α : Type
t : BTree α
⊢ mirror (mirror t) = t
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [mirror, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.mirror_mirror
Proof state before:
case empty
α : Type
⊢ mirror (mirror BTree.empty) = BTree.empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mirror_mirror
Proof state before:
case node
α : Type
a : α
l r : BTree α
ih_l : mirror (mirror l) = l
ih_r : mirror (mirror r) = r
⊢ mirror (mirror (BTree.node a l r)) = BTree.node a l r
Tactic:
simp [mirror, ih_l, ih_r]
Proof state after:
no goals
Theorem: LoVe.mirror_mirror_calc
Proof state before:
α : Type
⊢ mirror (mirror BTree.empty) = BTree.empty
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mirror_mirror_calc
Proof state before:
α : Type
a : α
l r : BTree α
⊢ mirror (mirror (BTree.node a l r)) = mirror (BTree.node a (mirror r) (mirror l))
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mirror_mirror_calc
Proof state before:
α : Type
a : α
l r : BTree α
⊢ mirror (BTree.node a (mirror r) (mirror l)) = BTree.node a (mirror (mirror l)) (mirror (mirror r))
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mirror_mirror_calc
Proof state before:
α : Type
a : α
l r : BTree α
⊢ BTree.node a (mirror (mirror l)) (mirror (mirror r)) = BTree.node a l (mirror (mirror r))
Tactic:
rw [mirror_mirror_calc l]
Proof state after:
no goals
Theorem: LoVe.mirror_mirror_calc
Proof state before:
α : Type
a : α
l r : BTree α
⊢ BTree.node a l (mirror (mirror r)) = BTree.node a l r
Tactic:
rw [mirror_mirror_calc r]
Proof state after:
no goals
Theorem: LoVe.mirror_Eq_empty_Iff
Proof state before:
α : Type
⊢ mirror BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
simp [mirror]
Proof state after:
no goals
Theorem: LoVe.mirror_Eq_empty_Iff
Proof state before:
α : Type
a✝² : α
a✝¹ a✝ : BTree α
⊢ mirror (BTree.node a✝² a✝¹ a✝) = BTree.empty ↔ BTree.node a✝² a✝¹ a✝ = BTree.empty
Tactic:
simp [mirror]
Proof state after:
no goals
Theorem: LoVe.length_listOfVec
Proof state before:
α : Type
⊢ List.length (listOfVec Vec.nil) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.length_listOfVec
Proof state before:
α : Type
a : α
n✝ : ℕ
v : Vec α n✝
⊢ List.length (listOfVec (Vec.cons a v)) = n✝ + 1
Tactic:
simp [listOfVec, length_listOfVec _ v]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.fst_of_two_props
Proof state before:
⊢ ∀ (a b : Prop), a → b → a
Tactic:
intro a b
Proof state after:
a b : Prop
⊢ a → b → a
Theorem: LoVe.BackwardProofs.fst_of_two_props
Proof state before:
a b : Prop
⊢ a → b → a
Tactic:
intro ha hb
Proof state after:
a b : Prop
ha : a
hb : b
⊢ a
Theorem: LoVe.BackwardProofs.fst_of_two_props
Proof state before:
a b : Prop
ha : a
hb : b
⊢ a
Tactic:
apply ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.fst_of_two_props_params
Proof state before:
a b : Prop
ha : a
hb : b
⊢ a
Tactic:
apply ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.prop_comp
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
⊢ a → c
Tactic:
intro ha
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Theorem: LoVe.BackwardProofs.prop_comp
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Tactic:
apply hbc
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ b
Theorem: LoVe.BackwardProofs.prop_comp
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ b
Tactic:
apply hab
Proof state after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.prop_comp
Proof state before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ a
Tactic:
apply ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.fst_of_two_props_exact
Proof state before:
a b : Prop
ha : a
hb : b
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.fst_of_two_props_assumption
Proof state before:
a b : Prop
ha : a
hb : b
⊢ a
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
a b : Prop
⊢ a ∧ b → b ∧ a
Tactic:
intro hab
Proof state after:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Tactic:
apply And.intro
Proof state after:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.right
Proof state after:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
exact hab
Proof state after:
case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.left
Proof state after:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop
Theorem: LoVe.BackwardProofs.And_swap
Proof state before:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop
Tactic:
exact hab
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
⊢ ∀ (a b : Prop), a ∧ b → b ∧ a
Tactic:
intro a b hab
Proof state after:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Tactic:
apply And.intro
Proof state after:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
{ exact And.right hab }
Proof state after:
case right
a b : Prop
hab : a ∧ b
⊢ a
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
{ exact And.left hab }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
case left
a b : Prop
hab : a ∧ b
⊢ b
Tactic:
exact And.right hab
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.And_swap_braces
Proof state before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
exact And.left hab
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.f5_if
Proof state before:
h : ∀ (n : ℕ), f n = n
⊢ f 5 = 5
Tactic:
exact h 5
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
a b : Prop
⊢ a ∨ b → b ∨ a
Tactic:
intro hab
Proof state after:
a b : Prop
hab : a ∨ b
⊢ b ∨ a
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
a b : Prop
hab : a ∨ b
⊢ b ∨ a
Tactic:
apply Or.elim hab
Proof state after:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a

case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a

case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
{ intro ha
  exact Or.inr ha }
Proof state after:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
{ intro hb
  exact Or.inl hb }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a
Tactic:
intro ha
Proof state after:
case left
a b : Prop
hab : a ∨ b
ha : a
⊢ b ∨ a
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case left
a b : Prop
hab : a ∨ b
ha : a
⊢ b ∨ a
Tactic:
exact Or.inr ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
intro hb
Proof state after:
case right
a b : Prop
hab : a ∨ b
hb : b
⊢ b ∨ a
Theorem: LoVe.BackwardProofs.Or_swap
Proof state before:
case right
a b : Prop
hab : a ∨ b
hb : b
⊢ b ∨ a
Tactic:
exact Or.inl hb
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.modus_ponens
Proof state before:
a b : Prop
⊢ (a → b) → a → b
Tactic:
intro hab ha
Proof state after:
a b : Prop
hab : a → b
ha : a
⊢ b
Theorem: LoVe.BackwardProofs.modus_ponens
Proof state before:
a b : Prop
hab : a → b
ha : a
⊢ b
Tactic:
apply hab
Proof state after:
a b : Prop
hab : a → b
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.modus_ponens
Proof state before:
a b : Prop
hab : a → b
ha : a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Not_Not_intro
Proof state before:
a : Prop
⊢ a → ¬¬a
Tactic:
intro ha hna
Proof state after:
a : Prop
ha : a
hna : ¬a
⊢ False
Theorem: LoVe.BackwardProofs.Not_Not_intro
Proof state before:
a : Prop
ha : a
hna : ¬a
⊢ False
Tactic:
apply hna
Proof state after:
a : Prop
ha : a
hna : ¬a
⊢ a
Theorem: LoVe.BackwardProofs.Not_Not_intro
Proof state before:
a : Prop
ha : a
hna : ¬a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Exists_double_iden
Proof state before:
⊢ ∃ n, double n = n
Tactic:
apply Exists.intro 0
Proof state after:
⊢ double 0 = 0
Theorem: LoVe.BackwardProofs.Exists_double_iden
Proof state before:
⊢ double 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.α_example
Proof state before:
α β : Type
f : α → β
⊢ (fun x => f x) = fun y => f y
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.β_example
Proof state before:
α β : Type
f : α → β
a : α
⊢ (fun x => f x) a = f a
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.δ_example
Proof state before:
⊢ double 5 = 5 + 5
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.ζ_example
Proof state before:
⊢ (let n := 2;
    n + n) =
    4
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.η_example
Proof state before:
α β : Type
f : α → β
⊢ (fun x => f x) = f
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.ι_example
Proof state before:
α β : Type
a : α
b : β
⊢ myProd.first (myProd.mk a b) = a
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = c
Tactic:
apply Eq.trans
Proof state after:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b

case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ ?b = c

case b
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ α
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b

case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ ?b = c

case b
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ α
Tactic:
{ exact hab }
Proof state after:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
{ apply Eq.symm
  exact hcb }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b
Tactic:
exact hab
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
apply Eq.symm
Proof state after:
case h₂.h
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ c = b
Theorem: LoVe.BackwardProofs.Eq_trans_symm
Proof state before:
case h₂.h
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ c = b
Tactic:
exact hcb
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Eq_trans_symm_rw
Proof state before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = c
Tactic:
rw [hab]
Proof state after:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Theorem: LoVe.BackwardProofs.Eq_trans_symm_rw
Proof state before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
rw [hcb]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
⊢ a → ¬¬a
Tactic:
rw [Not]
Proof state after:
a : Prop
⊢ a → ¬a → False
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
⊢ a → ¬a → False
Tactic:
rw [Not]
Proof state after:
a : Prop
⊢ a → (a → False) → False
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
⊢ a → (a → False) → False
Tactic:
intro ha
Proof state after:
a : Prop
ha : a
⊢ (a → False) → False
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
ha : a
⊢ (a → False) → False
Tactic:
intro hna
Proof state after:
a : Prop
ha : a
hna : a → False
⊢ False
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
ha : a
hna : a → False
⊢ False
Tactic:
apply hna
Proof state after:
a : Prop
ha : a
hna : a → False
⊢ a
Theorem: LoVe.BackwardProofs.a_proof_of_negation
Proof state before:
a : Prop
ha : a
hna : a → False
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.cong_two_args_1p1
Proof state before:
α : Type
a b c d : α
g : α → α → ℕ → α
hab : a = b
hcd : c = d
⊢ g a c (1 + 1) = g b d 2
Tactic:
simp [hab, hcd]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.abc_Eq_cba
Proof state before:
a b c : ℕ
⊢ a + b + c = c + b + a
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_zero
Proof state before:
n : ℕ
⊢ add 0 n = n
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_zero
Proof state before:
case zero

⊢ add 0 Nat.zero = Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_zero
Proof state before:
case succ
n' : ℕ
ih : add 0 n' = n'
⊢ add 0 (Nat.succ n') = Nat.succ n'
Tactic:
simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_succ
Proof state before:
m n : ℕ
⊢ add (Nat.succ m) n = Nat.succ (add m n)
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_succ
Proof state before:
case zero
m : ℕ
⊢ add (Nat.succ m) Nat.zero = Nat.succ (add m Nat.zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_succ
Proof state before:
case succ
m n' : ℕ
ih : add (Nat.succ m) n' = Nat.succ (add m n')
⊢ add (Nat.succ m) (Nat.succ n') = Nat.succ (add m (Nat.succ n'))
Tactic:
simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_comm
Proof state before:
m n : ℕ
⊢ add m n = add n m
Tactic:
induction n with
| zero       => simp [add, add_zero]
| succ n' ih => simp [add, add_succ, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_comm
Proof state before:
case zero
m : ℕ
⊢ add m Nat.zero = add Nat.zero m
Tactic:
simp [add, add_zero]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_comm
Proof state before:
case succ
m n' : ℕ
ih : add m n' = add n' m
⊢ add m (Nat.succ n') = add (Nat.succ n') m
Tactic:
simp [add, add_succ, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_assoc
Proof state before:
l m n : ℕ
⊢ add (add l m) n = add l (add m n)
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_assoc
Proof state before:
case zero
l m : ℕ
⊢ add (add l m) Nat.zero = add l (add m Nat.zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_assoc
Proof state before:
case succ
l m n' : ℕ
ih : add (add l m) n' = add l (add m n')
⊢ add (add l m) (Nat.succ n') = add l (add m (Nat.succ n'))
Tactic:
simp [add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_add
Proof state before:
l m n : ℕ
⊢ mul l (add m n) = add (mul l m) (mul l n)
Tactic:
induction n with
| zero       => rfl
| succ n' ih =>
  simp [add, mul, ih]
  ac_rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_add
Proof state before:
case zero
l m : ℕ
⊢ mul l (add m Nat.zero) = add (mul l m) (mul l Nat.zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_add
Proof state before:
case succ
l m n' : ℕ
ih : mul l (add m n') = add (mul l m) (mul l n')
⊢ mul l (add m (Nat.succ n')) = add (mul l m) (mul l (Nat.succ n'))
Tactic:
simp [add, mul, ih]
Proof state after:
case succ
l m n' : ℕ
ih : mul l (add m n') = add (mul l m) (mul l n')
⊢ add l (add (mul l m) (mul l n')) = add (mul l m) (add l (mul l n'))
Theorem: LoVe.BackwardProofs.mul_add
Proof state before:
case succ
l m n' : ℕ
ih : mul l (add m n') = add (mul l m) (mul l n')
⊢ add l (add (mul l m) (mul l n')) = add (mul l m) (add l (mul l n'))
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.cleanup_example
Proof state before:
a b c : Prop
ha : a
hb : b
hab : a → b
hbc : b → c
⊢ c
Tactic:
clear ha hab a
Proof state after:
b c : Prop
hb : b
hbc : b → c
⊢ c
Theorem: LoVe.BackwardProofs.cleanup_example
Proof state before:
b c : Prop
hb : b
hbc : b → c
⊢ c
Tactic:
apply hbc
Proof state after:
b c : Prop
hb : b
hbc : b → c
⊢ b
Theorem: LoVe.BackwardProofs.cleanup_example
Proof state before:
b c : Prop
hb : b
hbc : b → c
⊢ b
Tactic:
clear hbc c
Proof state after:
b : Prop
hb : b
⊢ b
Theorem: LoVe.BackwardProofs.cleanup_example
Proof state before:
b : Prop
hb : b
⊢ b
Tactic:
rename b => h
Proof state after:
b : Prop
h : b
⊢ b
Theorem: LoVe.BackwardProofs.cleanup_example
Proof state before:
b : Prop
h : b
⊢ b
Tactic:
exact h
Proof state after:
no goals
Theorem: LoVe.linarith_example
Proof state before:
i : ℤ
hi : i > 5
⊢ 2 * i + 3 > 11
Tactic:
linarith
Proof state after:
no goals
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
α : Type
R : α → α → Prop
⊢ Star (Star R) = Star R
Tactic:
apply funext
Proof state after:
case h
α : Type
R : α → α → Prop
⊢ ∀ (x : α), Star (Star R) x = Star R x
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
case h
α : Type
R : α → α → Prop
⊢ ∀ (x : α), Star (Star R) x = Star R x
Tactic:
intro a
Proof state after:
case h
α : Type
R : α → α → Prop
a : α
⊢ Star (Star R) a = Star R a
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
case h
α : Type
R : α → α → Prop
a : α
⊢ Star (Star R) a = Star R a
Tactic:
apply funext
Proof state after:
case h.h
α : Type
R : α → α → Prop
a : α
⊢ ∀ (x : α), Star (Star R) a x = Star R a x
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
case h.h
α : Type
R : α → α → Prop
a : α
⊢ ∀ (x : α), Star (Star R) a x = Star R a x
Tactic:
intro b
Proof state after:
case h.h
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b = Star R a b
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
case h.h
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b = Star R a b
Tactic:
apply propext
Proof state after:
case h.h.a
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b ↔ Star R a b
Theorem: LoVe.Star_Star_Eq_Star
Proof state before:
case h.h.a
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b ↔ Star R a b
Tactic:
apply Star_Star_Iff_Star
Proof state after:
no goals
Theorem: LoVe.cases_Eq_example
Proof state before:
α : Type
l r : α
h : l = r
P : α → α → Prop
⊢ P l r
Tactic:
cases h
Proof state after:
case refl
α : Type
l : α
P : α → α → Prop
⊢ P l l
Theorem: LoVe.cases_Eq_example
Proof state before:
case refl
α : Type
l : α
P : α → α → Prop
⊢ P l l
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.cases_Classical_em_example
Proof state before:
α : Type
a : α
P Q : α → Prop
⊢ Q a
Tactic:
have hor : P a ∨ ¬ P a :=
  Classical.em (P a)
Proof state after:
α : Type
a : α
P Q : α → Prop
hor : P a ∨ ¬P a
⊢ Q a
Theorem: LoVe.cases_Classical_em_example
Proof state before:
α : Type
a : α
P Q : α → Prop
hor : P a ∨ ¬P a
⊢ Q a
Tactic:
cases hor with
| inl hl => sorry
| inr hr => sorry
Proof state after:
no goals
Theorem: LoVe.cases_Classical_em_example
Proof state before:
case inl
α : Type
a : α
P Q : α → Prop
hl : P a
⊢ Q a
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.cases_Classical_em_example
Proof state before:
case inr
α : Type
a : α
P Q : α → Prop
hr : ¬P a
⊢ Q a
Tactic:
sorry
Proof state after:
no goals