internlm/Lean-Github huggingface dataset:
Theorem: LoVe.List.count_cons
Proof state before:
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
Tactic:
simp [hx]
Proof state after:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.countp (fun x_1 => x_1 == x) as + 1 = 1 + List.countp (fun x_1 => x_1 == x) as
Theorem: LoVe.List.count_cons
Proof state before:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.countp (fun x_1 => x_1 == x) as + 1 = 1 + List.countp (fun x_1 => x_1 == x) as
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.List.count_cons
Proof state before:
case inr
α : 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]
Proof state after:
case inr
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : ¬(a == x) = true
⊢ (bif a == x then List.countp.go (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.go (fun x_1 => x_1 == x) as 0
Theorem: LoVe.List.count_cons
Proof state before:
case inr
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : ¬(a == x) = true
⊢ (bif a == x then List.countp.go (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.go (fun x_1 => x_1 == x) as 0
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: LoVe.List.count_append
Proof state before:
α : Type
inst✝ : BEq α
x : α
as bs : List α
⊢ List.count x (as ++ bs) = List.count x as + List.count x bs
Tactic:
induction as with
| nil           => simp
| cons a as' ih =>
  simp [ih]
  ac_rfl
Proof state after:
no goals
Theorem: LoVe.List.count_append
Proof state before:
case nil
α : Type
inst✝ : BEq α
x : α
bs : List α
⊢ List.count x ([] ++ bs) = List.count x [] + List.count x bs
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.List.count_append
Proof state before:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ List.count x (a :: as' ++ bs) = List.count x (a :: as') + List.count x bs
Tactic:
simp [ih]
Proof state after:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ (bif a == x then 1 else 0) + (List.count x as' + List.count x bs) =
    (bif a == x then 1 else 0) + List.count x as' + List.count x bs
Theorem: LoVe.List.count_append
Proof state before:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ (bif a == x then 1 else 0) + (List.count x as' + List.count x bs) =
    (bif a == x then 1 else 0) + List.count x as' + List.count x bs
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.Set.Mem_empty
Proof state before:
α : Type
a : α
⊢ a ∈ ∅ ↔ False
Tactic:
simp [Membership.mem, Set.Mem, EmptyCollection.emptyCollection]
Proof state after:
no goals
Theorem: LoVe.Set.compreh_False
Proof state before:
α : Type
⊢ {a | False} = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.subseteq_def
Proof state before:
α : Type
A B : Set α
⊢ A ⊆ B ↔ ∀ (a : α), a ∈ A → a ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.Mem_singleton
Proof state before:
α : Type
a b : α
⊢ a ∈ {b} ↔ a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.Mem_compreh
Proof state before:
α : Type
A : Set α
⊢ {a | a ∈ A} = A
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.compreh_Mem
Proof state before:
α : Type
a : α
P : α → Prop
⊢ a ∈ {a | P a} ↔ P a
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.empty_union
Proof state before:
α : Type
A : Set α
⊢ ∅ ∪ A = A
Tactic:
simp [Union.union, Set.union]
Proof state after:
no goals
Theorem: LoVe.Set.union_empty
Proof state before:
α : Type
A : Set α
⊢ A ∪ ∅ = A
Tactic:
simp [Union.union, Set.union]
Proof state after:
no goals
Theorem: LoVe.Set.Mem_union
Proof state before:
α : Type
a : α
A B : Set α
⊢ a ∈ A ∪ B ↔ a ∈ A ∨ a ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.unordered_pair_comm
Proof state before:
α : Type
a b : α
⊢ {a, b} = {b, a}
Tactic:
apply Set.ext
Proof state after:
case h
α : Type
a b : α
⊢ ∀ (x : α), x ∈ {a, b} ↔ x ∈ {b, a}
Theorem: LoVe.Set.unordered_pair_comm
Proof state before:
case h
α : Type
a b : α
⊢ ∀ (x : α), x ∈ {a, b} ↔ x ∈ {b, a}
Tactic:
simp [insert, singleton, Set.insert, Set.singleton]
Proof state after:
case h
α : Type
a b : α
⊢ ∀ (x : α), x = a ∨ x = b ↔ x = b ∨ x = a
Theorem: LoVe.Set.unordered_pair_comm
Proof state before:
case h
α : Type
a b : α
⊢ ∀ (x : α), x = a ∨ x = b ↔ x = b ∨ x = a
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.Set.le_def
Proof state before:
α : Type
A B : Set α
⊢ A ≤ B ↔ A ⊆ B
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Set.lt_def
Proof state before:
α : Type
A B : Set α
⊢ A < B ↔ A ⊆ B ∧ A ≠ B
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mem_Id
Proof state before:
α : Type
a b : α
⊢ (a, b) ∈ Id ↔ b = a
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mem_comp
Proof state before:
α : Type
r₁ r₂ : Set (α × α)
a b : α
⊢ (a, b) ∈ r₁ ◯ r₂ ↔ ∃ c, (a, c) ∈ r₁ ∧ (c, b) ∈ r₂
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.mem_restrict
Proof state before:
α : Type
r : Set (α × α)
P : α → Prop
a b : α
⊢ (a, b) ∈ r ⇃ P ↔ (a, b) ∈ r ∧ P a
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.RTC.trans
Proof state before:
α : Type
R : α → α → Prop
a b c : α
hab : RTC R a b
hbc : RTC R b c
⊢ RTC R a c
Tactic:
induction hbc with
| refl =>
  assumption
| tail c d hbc hcd hac =>
  apply tail <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.RTC.trans
Proof state before:
case refl
α : Type
R : α → α → Prop
a b c : α
hab : RTC R a b
⊢ RTC R a b
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.RTC.trans
Proof state before:
case tail
α : Type
R : α → α → Prop
a b c✝ : α
hab : RTC R a b
c d : α
hbc : RTC R b c
hcd : R c d
hac : RTC R a c
⊢ RTC R a d
Tactic:
apply tail <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.RTC.head
Proof state before:
α : Type
R : α → α → Prop
a b c : α
hab : R a b
hbc : RTC R b c
⊢ RTC R a c
Tactic:
induction hbc with
| refl =>
  exact tail _ _ refl hab
| tail c d hbc hcd hac =>
  apply tail <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.RTC.head
Proof state before:
case refl
α : Type
R : α → α → Prop
a b c : α
hab : R a b
⊢ RTC R a b
Tactic:
exact tail _ _ refl hab
Proof state after:
no goals
Theorem: LoVe.RTC.head
Proof state before:
case tail
α : Type
R : α → α → Prop
a b c✝ : α
hab : R a b
c d : α
hbc : RTC R b c
hcd : R c d
hac : RTC R a c
⊢ RTC R a d
Tactic:
apply tail <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.RTC.head_induction_on
Proof state before:
α : Type
R : α → α → Prop
b : α
P : (a : α) → RTC R a b → Prop
a : α
h : RTC R a b
refl : P b (_ : RTC R b b)
head : ∀ (a c : α) (h' : R a c) (h : RTC R c b), P c h → P a (_ : RTC R a b)
⊢ P a h
Tactic:
induction h with
| refl =>
  exact refl
| tail b' c _ hb'c ih =>
  apply ih (P := fun a hab' ↦ P a (RTC.tail _ _ hab' hb'c))
  { exact head _ _ hb'c _ refl }
  { intro x y hxy hyb' hy
    exact head _ _ hxy _ hy }
Proof state after:
no goals
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case refl
α : Type
R : α → α → Prop
b a : α
P : (a_1 : α) → RTC R a_1 a → Prop
refl : P a (_ : RTC R a a)
head : ∀ (a_1 c : α) (h' : R a_1 c) (h : RTC R c a), P c h → P a_1 (_ : RTC R a_1 a)
⊢ P a (_ : RTC R a a)
Tactic:
exact refl
Proof state after:
no goals
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P a (_ : RTC R a c)
Tactic:
apply ih (P := fun a hab' ↦ P a (RTC.tail _ _ hab' hb'c))
Proof state after:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)

case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)

case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
{ exact head _ _ hb'c _ refl }
Proof state after:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
{ intro x y hxy hyb' hy
  exact head _ _ hxy _ hy }
Proof state after:
no goals
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail.refl
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ P b' (_ : RTC R b' c)
Tactic:
exact head _ _ hb'c _ refl
Proof state after:
no goals
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
⊢ ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 b'), P c_1 (_ : RTC R c_1 c) → P a (_ : RTC R a c)
Tactic:
intro x y hxy hyb' hy
Proof state after:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
x y : α
hxy : R x y
hyb' : RTC R y b'
hy : P y (_ : RTC R y c)
⊢ P x (_ : RTC R x c)
Theorem: LoVe.RTC.head_induction_on
Proof state before:
case tail.head
α : Type
R : α → α → Prop
b a b' c : α
hab : RTC R a b'
hb'c : R b' c
ih :
  ∀ {P : (a : α) → RTC R a b' → Prop},
    P b' (_ : RTC R b' b') → (∀ (a c : α) (h' : R a c) (h : RTC R c b'), P c h → P a (_ : RTC R a b')) → P a hab
P : (a : α) → RTC R a c → Prop
refl : P c (_ : RTC R c c)
head : ∀ (a c_1 : α) (h' : R a c_1) (h : RTC R c_1 c), P c_1 h → P a (_ : RTC R a c)
x y : α
hxy : R x y
hyb' : RTC R y b'
hy : P y (_ : RTC R y c)
⊢ P x (_ : RTC R x c)
Tactic:
exact head _ _ hxy _ hy
Proof state after:
no goals
Theorem: LoVe.RTC.lift
Proof state before:
α β : Type
R : α → α → Prop
S : β → β → Prop
a b : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
hab : RTC R a b
⊢ RTC S (f a) (f b)
Tactic:
induction hab with
| refl => apply refl
| tail b c hab hbc ih =>
  apply tail
  apply ih
  apply hf
  exact hbc
Proof state after:
no goals
Theorem: LoVe.RTC.lift
Proof state before:
case refl
α β : Type
R : α → α → Prop
S : β → β → Prop
a b : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
⊢ RTC S (f a) (f a)
Tactic:
apply refl
Proof state after:
no goals
Theorem: LoVe.RTC.lift
Proof state before:
case tail
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) (f c)
Tactic:
apply tail
Proof state after:
case tail.hab
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) ?tail.b

case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S ?tail.b (f c)

case tail.b
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ β
Theorem: LoVe.RTC.lift
Proof state before:
case tail.hab
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) ?tail.b

case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S ?tail.b (f c)

case tail.b
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ β
Tactic:
apply ih
Proof state after:
case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S (f b) (f c)
Theorem: LoVe.RTC.lift
Proof state before:
case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S (f b) (f c)
Tactic:
apply hf
Proof state after:
case tail.hbc.a
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ R b c
Theorem: LoVe.RTC.lift
Proof state before:
case tail.hbc.a
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ R b c
Tactic:
exact hbc
Proof state after:
no goals
Theorem: LoVe.RTC.RTC_RTC_eq
Proof state before:
α : Type
R : α → α → Prop
a b : α
h : RTC (RTC R) a b
⊢ RTC R a b
Tactic:
induction h with
| refl => exact refl
| tail b c hab' hbc ih =>
  apply trans <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.RTC.RTC_RTC_eq
Proof state before:
case refl
α : Type
R : α → α → Prop
a b : α
⊢ RTC R a a
Tactic:
exact refl
Proof state after:
no goals
Theorem: LoVe.RTC.RTC_RTC_eq
Proof state before:
case tail
α : Type
R : α → α → Prop
a b✝ b c : α
hab' : RTC (RTC R) a b
hbc : RTC R b c
ih : RTC R a b
⊢ RTC R a c
Tactic:
apply trans <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.update_apply
Proof state before:
name : String
val : ℕ
s : State
⊢ State.update name val s name = val
Tactic:
apply if_pos
Proof state after:
case hc
name : String
val : ℕ
s : State
⊢ name = name
Theorem: LoVe.update_apply
Proof state before:
case hc
name : String
val : ℕ
s : State
⊢ name = name
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.update_apply_neq
Proof state before:
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ State.update name val s name' = s name'
Tactic:
apply if_neg
Proof state after:
case hnc
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ ¬name' = name
Theorem: LoVe.update_apply_neq
Proof state before:
case hnc
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ ¬name' = name
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.update_override
Proof state before:
name : String
val₁ val₂ : ℕ
s : State
⊢ State.update name val₁ (State.update name val₂ s) = State.update name val₁ s
Tactic:
apply funext
Proof state after:
case h
name : String
val₁ val₂ : ℕ
s : State
⊢ ∀ (x : String), State.update name val₁ (State.update name val₂ s) x = State.update name val₁ s x
Theorem: LoVe.update_override
Proof state before:
case h
name : String
val₁ val₂ : ℕ
s : State
⊢ ∀ (x : String), State.update name val₁ (State.update name val₂ s) x = State.update name val₁ s x
Tactic:
intro name'
Proof state after:
case h
name : String
val₁ val₂ : ℕ
s : State
name' : String
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Theorem: LoVe.update_override
Proof state before:
case h
name : String
val₁ val₂ : ℕ
s : State
name' : String
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
cases Classical.em (name' = name) with
| inl h => simp [h]
| inr h => simp [h]
Proof state after:
no goals
Theorem: LoVe.update_override
Proof state before:
case h.inl
name : String
val₁ val₂ : ℕ
s : State
name' : String
h : name' = name
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LoVe.update_override
Proof state before:
case h.inr
name : String
val₁ val₂ : ℕ
s : State
name' : String
h : ¬name' = name
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LoVe.update_swap
Proof state before:
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) = State.update name₂ val₂ (State.update name₁ val₁ s)
Tactic:
apply funext
Proof state after:
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
⊢ ∀ (x : String),
    State.update name₁ val₁ (State.update name₂ val₂ s) x = State.update name₂ val₂ (State.update name₁ val₁ s) x
Theorem: LoVe.update_swap
Proof state before:
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
⊢ ∀ (x : String),
    State.update name₁ val₁ (State.update name₂ val₂ s) x = State.update name₂ val₂ (State.update name₁ val₁ s) x
Tactic:
intro name'
Proof state after:
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Theorem: LoVe.update_swap
Proof state before:
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Tactic:
cases Classical.em (name' = name₁) with
| inl h => simp [*]
| inr h =>
  cases Classical.em (name' = name₁) with
  | inl h => simp [*]
  | inr h => simp [State.update, *]
Proof state after:
no goals
Theorem: LoVe.update_swap
Proof state before:
case h.inl
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
h : name' = name₁
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.update_swap
Proof state before:
case h.inr
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
h : ¬name' = name₁
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Tactic:
cases Classical.em (name' = name₁) with
| inl h => simp [*]
| inr h => simp [State.update, *]
Proof state after:
no goals
Theorem: LoVe.update_swap
Proof state before:
case h.inr.inl
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
h✝ : ¬name' = name₁
h : name' = name₁
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.update_swap
Proof state before:
case h.inr.inr
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
h✝ h : ¬name' = name₁
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
Tactic:
simp [State.update, *]
Proof state after:
no goals
Theorem: LoVe.update_id
Proof state before:
name : String
s : State
⊢ State.update name (s name) s = s
Tactic:
apply funext
Proof state after:
case h
name : String
s : State
⊢ ∀ (x : String), State.update name (s name) s x = s x
Theorem: LoVe.update_id
Proof state before:
case h
name : String
s : State
⊢ ∀ (x : String), State.update name (s name) s x = s x
Tactic:
intro name'
Proof state after:
case h
name : String
s : State
name' : String
⊢ State.update name (s name) s name' = s name'
Theorem: LoVe.update_id
Proof state before:
case h
name : String
s : State
name' : String
⊢ State.update name (s name) s name' = s name'
Tactic:
simp [State.update]
Proof state after:
case h
name : String
s : State
name' : String
⊢ name' = name → s name = s name'
Theorem: LoVe.update_id
Proof state before:
case h
name : String
s : State
name' : String
⊢ name' = name → s name = s name'
Tactic:
intro heq
Proof state after:
case h
name : String
s : State
name' : String
heq : name' = name
⊢ s name = s name'
Theorem: LoVe.update_id
Proof state before:
case h
name : String
s : State
name' : String
heq : name' = name
⊢ s name = s name'
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.update_same_const
Proof state before:
name : String
val : ℕ
⊢ (State.update name val fun x => val) = fun x => val
Tactic:
apply funext
Proof state after:
case h
name : String
val : ℕ
⊢ ∀ (x : String), State.update name val (fun x => val) x = val
Theorem: LoVe.update_same_const
Proof state before:
case h
name : String
val : ℕ
⊢ ∀ (x : String), State.update name val (fun x => val) x = val
Tactic:
simp [State.update]
Proof state after:
no goals
Theorem: LoVe.mmap_append
Proof state before:
m : Type → Type
inst✝ : LawfulMonad m
α β : Type
f : α → m β
x✝ : List α
⊢ mmap f ([] ++ x✝) = do
    let bs ← mmap f []
    let bs' ← mmap f x✝
    pure (bs ++ bs')
Tactic:
simp [mmap, LawfulMonad.bind_pure, LawfulMonad.pure_bind]
Proof state after:
no goals