internlm/Lean-Github huggingface dataset:
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬f x_1 = x•
Tactic:
lib_rewrite [1, 1, 1, 2, 0, 1] Set.ext_iff [1, 1, 1, 1, 1, 2]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬(∀ x_2⋆ : X⠀
    x_2⋆ ∈ f x_1 ↔ x_2⋆ ∈ x•)
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X⠀
  ¬(∀ x_2⋆ : X⠀
    x_2⋆ ∈ f x_1 ↔ x_2⋆ ∈ x•)
Tactic:
tree_push_neg [1, 1, 1, 1]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬(x_2• ∈ f x_1 ↔ x_2• ∈ x•)
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬(x_2• ∈ f x_1 ↔ x_2• ∈ x•)
Tactic:
lib_rewrite [1, 1, 2, 0, 1] not_iff [1, 1, 1, 1, 1]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬x_2• ∈ f x_1 ↔ x_2• ∈ x•
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ x_1 : X, ∃ x_2• : X⠀
  ¬x_2• ∈ f x_1 ↔ x_2• ∈ x•
Tactic:
unify_forall_exists [1, 1, 1]
Proof state after:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ a : X⠀
  ¬a ∈ f a ↔ a ∈ x•
Theorem: Cantor
Proof state before:
⊢ ∀ X : Type u, f : X → Set X, ∃ x• : Set X, ∀ a : X⠀
  ¬a ∈ f a ↔ a ∈ x•
Tactic:
lib_apply refl [1, 1, 1, 1, 2]
Proof state after:
no goals
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) ↔ ∃ a, p → q a
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Tactic:
by_cases p
Proof state after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a
Tactic:
intro g
Proof state after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a
Tactic:
have ⟨a, g⟩ := g ‹p›
Proof state after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g✝ : Imp p (_root_.Exists q)
a : α
g : q a
⊢ ∃ a, p → q a
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g✝ : Imp p (_root_.Exists q)
a : α
g : q a
⊢ ∃ a, p → q a
Tactic:
exact ⟨a, fun _ => g⟩
Proof state after:
no goals
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a
Tactic:
intro _
Proof state after:
case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
a✝ : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Tactic:
intro ⟨a, h⟩ g
Proof state after:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
a : α
h : p → q a
g : p
⊢ _root_.Exists q
Theorem: MotivatedTree.imp_exists_iff
Proof state before:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
a : α
h : p → q a
g : p
⊢ _root_.Exists q
Tactic:
exact ⟨a, h g⟩
Proof state after:
no goals
Theorem: cantor_end
Proof state before:
⊢ ∀ (X : Type u) (f : X → Set X), ∃ a, ∀ (a_1 : X), a_1 ∉ f a_1 ↔ a_1 ∈ a
Tactic:
make_tree
Proof state after:
⊢ MotivatedTree.Forall (Type u) fun X =>
    MotivatedTree.Forall (X → Set X) fun f =>
      MotivatedTree.Exists (Set X) fun a => MotivatedTree.Forall X fun a_1 => MotivatedTree.Not (a_1 ∈ f a_1) ↔ a_1 ∈ a
Theorem: cantor_end
Proof state before:
⊢ MotivatedTree.Forall (Type u) fun X =>
    MotivatedTree.Forall (X → Set X) fun f =>
      MotivatedTree.Exists (Set X) fun a => MotivatedTree.Forall X fun a_1 => MotivatedTree.Not (a_1 ∈ f a_1) ↔ a_1 ∈ a
Tactic:
lib_apply [1,1,1,1] refl [1, 1, 1, 1, 2]
Proof state after:
no goals
Theorem: LoVe.Nat.two_mul
Proof state before:
n : ℕ
⊢ 2 * n = n + n
Tactic:
ring
Proof state after:
no goals
Theorem: LoVe.Nat.add_sub_again
Proof state before:
m n : ℕ
⊢ m + n - m = n
Tactic:
induction m with
| zero => simp
| succ m' ih => rw [Nat.succ_add, Nat.succ_sub_succ, ih]
Proof state after:
no goals
Theorem: LoVe.Nat.add_sub_again
Proof state before:
case zero
n : ℕ
⊢ Nat.zero + n - Nat.zero = n
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Nat.add_sub_again
Proof state before:
case succ
n m' : ℕ
ih : m' + n - m' = n
⊢ Nat.succ m' + n - Nat.succ m' = n
Tactic:
rw [Nat.succ_add, Nat.succ_sub_succ, ih]
Proof state after:
no goals
Theorem: LoVe.Nat.sub_one_add
Proof state before:
n m : ℕ
h : ¬n = 0
⊢ n - 1 + m = n + m - 1
Tactic:
induction n with
| zero => aesop
| succ =>
  rw [Nat.succ_add]
  aesop
Proof state after:
no goals
Theorem: LoVe.Nat.sub_one_add
Proof state before:
case zero
m : ℕ
h : ¬Nat.zero = 0
⊢ Nat.zero - 1 + m = Nat.zero + m - 1
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.Nat.sub_one_add
Proof state before:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ n_1 + m - 1
Tactic:
rw [Nat.succ_add]
Proof state after:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ (n_1 + m) - 1
Theorem: LoVe.Nat.sub_one_add
Proof state before:
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ (n_1 + m) - 1
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
l m n : ℕ
⊢ m + l < n + l ↔ m < n
Tactic:
apply Iff.intro
Proof state after:
case mp
l m n : ℕ
⊢ m + l < n + l → m < n

case mpr
l m n : ℕ
⊢ m < n → m + l < n + l
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mp
l m n : ℕ
⊢ m + l < n + l → m < n

case mpr
l m n : ℕ
⊢ m < n → m + l < n + l
Tactic:
{ intro h
  apply Nat.lt_of_add_lt_add_right h }
Proof state after:
case mpr
l m n : ℕ
⊢ m < n → m + l < n + l
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mpr
l m n : ℕ
⊢ m < n → m + l < n + l
Tactic:
{ intro h
  apply Nat.add_lt_add_right h }
Proof state after:
no goals
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mp
l m n : ℕ
⊢ m + l < n + l → m < n
Tactic:
intro h
Proof state after:
case mp
l m n : ℕ
h : m + l < n + l
⊢ m < n
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mp
l m n : ℕ
h : m + l < n + l
⊢ m < n
Tactic:
apply Nat.lt_of_add_lt_add_right h
Proof state after:
no goals
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mpr
l m n : ℕ
⊢ m < n → m + l < n + l
Tactic:
intro h
Proof state after:
case mpr
l m n : ℕ
h : m < n
⊢ m + l < n + l
Theorem: LoVe.Nat.plus_lt_plus_right
Proof state before:
case mpr
l m n : ℕ
h : m < n
⊢ m + l < n + l
Tactic:
apply Nat.add_lt_add_right h
Proof state after:
no goals
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
l m n : ℕ
⊢ m + l ≤ n + l ↔ m ≤ n
Tactic:
apply Iff.intro
Proof state after:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n

case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n

case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
{ intro h
  apply Nat.le_of_add_le_add_right h }
Proof state after:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
{ intro h
  apply Nat.add_le_add_right h }
Proof state after:
no goals
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n
Tactic:
intro h
Proof state after:
case mp
l m n : ℕ
h : m + l ≤ n + l
⊢ m ≤ n
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mp
l m n : ℕ
h : m + l ≤ n + l
⊢ m ≤ n
Tactic:
apply Nat.le_of_add_le_add_right h
Proof state after:
no goals
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
intro h
Proof state after:
case mpr
l m n : ℕ
h : m ≤ n
⊢ m + l ≤ n + l
Theorem: LoVe.Nat.plus_le_plus_right
Proof state before:
case mpr
l m n : ℕ
h : m ≤ n
⊢ m + l ≤ n + l
Tactic:
apply Nat.add_le_add_right h
Proof state after:
no goals
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
m n : ℕ
p : Prop
hge : m ≥ n
⊢ m < n → p ↔ True
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True

case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True

case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
{ intro himp
  apply True.intro }
Proof state after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
{ intro htrue
  intro hlt
  have hle : n ≤ m :=
    hge
  rw [←Nat.not_lt_eq] at hle
  apply False.elim
  exact hle hlt }
Proof state after:
no goals
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
⊢ (m < n → p) → True
Tactic:
intro himp
Proof state after:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
himp : m < n → p
⊢ True
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mp
m n : ℕ
p : Prop
hge : m ≥ n
himp : m < n → p
⊢ True
Tactic:
apply True.intro
Proof state after:
no goals
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
⊢ True → m < n → p
Tactic:
intro htrue
Proof state after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
⊢ m < n → p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
⊢ m < n → p
Tactic:
intro hlt
Proof state after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
⊢ p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
⊢ p
Tactic:
have hle : n ≤ m :=
  hge
Proof state after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : n ≤ m
⊢ p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : n ≤ m
⊢ p
Tactic:
rw [←Nat.not_lt_eq] at hle
Proof state after:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ p
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ p
Tactic:
apply False.elim
Proof state after:
case mpr.h
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ False
Theorem: LoVe.Nat.le_lt_imp
Proof state before:
case mpr.h
m n : ℕ
p : Prop
hge : m ≥ n
htrue : True
hlt : m < n
hle : ¬m < n
⊢ False
Tactic:
exact hle hlt
Proof state after:
no goals
Theorem: LoVe.Nat.lt_succ
Proof state before:
m n : ℕ
⊢ Nat.succ m < Nat.succ n ↔ m < n
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n

case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Theorem: LoVe.Nat.lt_succ
Proof state before:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n

case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
{ apply Nat.lt_of_succ_lt_succ }
Proof state after:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Theorem: LoVe.Nat.lt_succ
Proof state before:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
{ apply Nat.succ_lt_succ }
Proof state after:
no goals
Theorem: LoVe.Nat.lt_succ
Proof state before:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n
Tactic:
apply Nat.lt_of_succ_lt_succ
Proof state after:
no goals
Theorem: LoVe.Nat.lt_succ
Proof state before:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
apply Nat.succ_lt_succ
Proof state after:
no goals
Theorem: LoVe.Nat.le_succ
Proof state before:
m n : ℕ
⊢ Nat.succ m ≤ Nat.succ n ↔ m ≤ n
Tactic:
apply Iff.intro
Proof state after:
case mp
m n : ℕ
⊢ Nat.succ m ≤ Nat.succ n → m ≤ n

case mpr
m n : ℕ
⊢ m ≤ n → Nat.succ m ≤ Nat.succ n
Theorem: LoVe.Nat.le_succ
Proof state before:
case mp
m n : ℕ
⊢ Nat.succ m ≤ Nat.succ n → m ≤ n

case mpr
m n : ℕ
⊢ m ≤ n → Nat.succ m ≤ Nat.succ n
Tactic:
{ apply Nat.le_of_succ_le_succ }
Proof state after:
case mpr
m n : ℕ
⊢ m ≤ n → Nat.succ m ≤ Nat.succ n
Theorem: LoVe.Nat.le_succ
Proof state before:
case mpr
m n : ℕ
⊢ m ≤ n → Nat.succ m ≤ Nat.succ n
Tactic:
{ apply Nat.succ_le_succ }
Proof state after:
no goals
Theorem: LoVe.Nat.le_succ
Proof state before:
case mp
m n : ℕ
⊢ Nat.succ m ≤ Nat.succ n → m ≤ n
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: LoVe.Nat.le_succ
Proof state before:
case mpr
m n : ℕ
⊢ m ≤ n → Nat.succ m ≤ Nat.succ n
Tactic:
apply Nat.succ_le_succ
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
⊢ Int.neg ∘ Int.neg = id
Tactic:
apply funext
Proof state after:
case h

⊢ ∀ (x : ℤ), (Int.neg ∘ Int.neg) x = id x
Theorem: LoVe.Int.neg_neg
Proof state before:
case h

⊢ ∀ (x : ℤ), (Int.neg ∘ Int.neg) x = id x
Tactic:
intro i
Proof state after:
case h
i : ℤ
⊢ (Int.neg ∘ Int.neg) i = id i
Theorem: LoVe.Int.neg_neg
Proof state before:
case h
i : ℤ
⊢ (Int.neg ∘ Int.neg) i = id i
Tactic:
simp
Proof state after:
case h
i : ℤ
⊢ Int.neg (Int.neg i) = i
Theorem: LoVe.Int.neg_neg
Proof state before:
case h
i : ℤ
⊢ Int.neg (Int.neg i) = i
Tactic:
cases i with
| ofNat n =>
  { simp [Int.neg]
    cases n
    { simp }
    { simp [Int.negOfNat] } }
| negSucc n =>
  { simp [Int.neg]
    have hnp1 : (↑n + 1 : ℤ) = ↑(n + 1) :=
      by simp
    rw [hnp1]
    rfl }
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat
n : ℕ
⊢ Int.neg (Int.neg (Int.ofNat n)) = Int.ofNat n
Tactic:
simp [Int.neg]
Proof state after:
case h.ofNat
n : ℕ
⊢ (match Int.negOfNat n with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑n
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat
n : ℕ
⊢ (match Int.negOfNat n with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑n
Tactic:
cases n
Proof state after:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero

case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero

case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
{ simp }
Proof state after:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
{ simp [Int.negOfNat] }
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
Tactic:
simp [Int.negOfNat]
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.negSucc
n : ℕ
⊢ Int.neg (Int.neg (Int.negSucc n)) = Int.negSucc n
Tactic:
simp [Int.neg]
Proof state after:
case h.negSucc
n : ℕ
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.negSucc
n : ℕ
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
have hnp1 : (↑n + 1 : ℤ) = ↑(n + 1) :=
  by simp
Proof state after:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑n + 1 with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
rw [hnp1]
Proof state after:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑(n + 1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Theorem: LoVe.Int.neg_neg
Proof state before:
case h.negSucc
n : ℕ
hnp1 : ↑n + 1 = ↑(n + 1)
⊢ (match ↑(n + 1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    Int.negSucc n
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Int.neg_neg
Proof state before:
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Int.zero_eq_mul
Proof state before:
a b : ℤ
⊢ 0 = a * b ↔ a = 0 ∨ b = 0
Tactic:
rw [eq_comm]
Proof state after:
a b : ℤ
⊢ a * b = 0 ↔ a = 0 ∨ b = 0
Theorem: LoVe.Int.zero_eq_mul
Proof state before:
a b : ℤ
⊢ a * b = 0 ↔ a = 0 ∨ b = 0
Tactic:
exact Int.mul_eq_zero
Proof state after:
no goals
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
⊢ x / 2 + x / 2 = x
Tactic:
have hxx : x + x = 2 * x :=
  by linarith
Proof state after:
x : ℚ
hxx : x + x = 2 * x
⊢ x / 2 + x / 2 = x
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
⊢ x / 2 + x / 2 = x
Tactic:
have hxx2 : (x + x) / 2 = (2 * x) / 2 :=
  by rw [hxx]
Proof state after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Tactic:
have hx2x2 : x / 2 + x / 2 = (2 * x) / 2 :=
  by
    rw [←hxx2]
    rw [add_div]
Proof state after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Tactic:
rw [hx2x2]
Proof state after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ 2 * x / 2 = x
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ 2 * x / 2 = x
Tactic:
ring
Proof state after:
no goals
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
⊢ x + x = 2 * x
Tactic:
linarith
Proof state after:
no goals
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
⊢ (x + x) / 2 = 2 * x / 2
Tactic:
rw [hxx]
Proof state after:
no goals
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = 2 * x / 2
Tactic:
rw [←hxx2]
Proof state after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = (x + x) / 2
Theorem: LoVe.Rat.div_two_add_div_two
Proof state before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = (x + x) / 2
Tactic:
rw [add_div]
Proof state after:
no goals
Theorem: LoVe.List.count_nil
Proof state before:
α : Type
inst✝ : BEq α
x : α
⊢ List.count x [] = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.List.countp.go_accum
Proof state before:
α : Type
p : α → Bool
as : List α
acc : ℕ
⊢ List.countp.go p as acc = List.countp p as + acc
Tactic:
induction as generalizing acc with
| nil           => simp [List.countp.go, List.countp]
| cons a as' ih =>
  simp [List.countp, List.countp.go]
  cases Classical.em (p a) with
  | inl hp =>
    simp [hp, ih]
    ac_rfl
  | inr hp => simp [hp, ih]
Proof state after:
no goals
Theorem: LoVe.List.countp.go_accum
Proof state before:
case nil
α : Type
p : α → Bool
acc : ℕ
⊢ List.countp.go p [] acc = List.countp p [] + acc
Tactic:
simp [List.countp.go, List.countp]
Proof state after:
no goals
Theorem: LoVe.List.countp.go_accum
Proof state before:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ List.countp.go p (a :: as') acc = List.countp p (a :: as') + acc
Tactic:
simp [List.countp, List.countp.go]
Proof state after:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Theorem: LoVe.List.countp.go_accum
Proof state before:
case cons
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
cases Classical.em (p a) with
| inl hp =>
  simp [hp, ih]
  ac_rfl
| inr hp => simp [hp, ih]
Proof state after:
no goals
Theorem: LoVe.List.countp.go_accum
Proof state before:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
simp [hp, ih]
Proof state after:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ List.countp p as' + (acc + 1) = List.countp p as' + 1 + acc
Theorem: LoVe.List.countp.go_accum
Proof state before:
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ List.countp p as' + (acc + 1) = List.countp p as' + 1 + acc
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.List.countp.go_accum
Proof state before:
case cons.inr
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : ¬p a = true
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
Tactic:
simp [hp, ih]
Proof state after:
no goals
Theorem: LoVe.List.count_cons
Proof state before:
α : Type
inst✝ : BEq α
x a : α
as : List α
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
Tactic:
cases Classical.em (a == x) with
| inl hx =>
  rw [List.count, List.countp, List.countp.go, List.countp.go_accum]
  simp [hx]
  ac_rfl
| inr hx =>
  rw [List.count, List.countp, List.countp.go, List.countp]
  simp [hx]
Proof state after:
no goals
Theorem: LoVe.List.count_cons
Proof state before:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
Tactic:
rw [List.count, List.countp, List.countp.go, List.countp.go_accum]
Proof state after:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ (bif a == x then List.countp (fun x_1 => x_1 == x) as + (0 + 1) else List.countp.go (fun x_1 => x_1 == x) as 0) =
    (bif a == x then 1 else 0) + List.countp (fun x_1 => x_1 == x) as