internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof state before:
case if_true
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : B s
s₂ : State
⊢ (S, s) ⟹ s₂ → (Stmt.ifThenElse B S T, s) ⟹ s₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof state before:
case if_false
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : ¬B s
s₂ : State
⊢ (T, s) ⟹ s₂ → (Stmt.ifThenElse B S T, s) ⟹ s₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_of_SmallStep_of_BigStep
Proof state before:
case whileDo
Ss₀ Ss₁ : Stmt × State
B : State → Prop
S : Stmt
s s₂ : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ s₂ → (Stmt.whileDo B S, s) ⟹ s₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
Ss : Stmt × State
t : State
⊢ RTC SmallStep Ss (Stmt.skip, t) → Ss ⟹ t
Tactic:
intro hS
Proof state after:
Ss : Stmt × State
t : State
hS : RTC SmallStep Ss (Stmt.skip, t)
⊢ Ss ⟹ t
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
Ss : Stmt × State
t : State
hS : RTC SmallStep Ss (Stmt.skip, t)
⊢ Ss ⟹ t
Tactic:
induction hS using RTC.head_induction_on with
| refl =>
  apply BigStep.skip
| head Ss Ss' hST hsmallT ih =>
  cases Ss' with
  | mk S' s' =>
    apply BigStep_of_SmallStep_of_BigStep hST
    apply ih
Proof state after:
no goals
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
case refl
Ss : Stmt × State
t : State
⊢ (Stmt.skip, t) ⟹ t
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
case head
Ss✝ : Stmt × State
t : State
Ss Ss' : Stmt × State
hST : Ss ⇒ Ss'
hsmallT : RTC SmallStep Ss' (Stmt.skip, t)
ih : Ss' ⟹ t
⊢ Ss ⟹ t
Tactic:
cases Ss' with
| mk S' s' =>
  apply BigStep_of_SmallStep_of_BigStep hST
  apply ih
Proof state after:
no goals
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ Ss ⟹ t
Tactic:
apply BigStep_of_SmallStep_of_BigStep hST
Proof state after:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ (S', s') ⟹ t
Theorem: LoVe.BigStep_of_RTC_SmallStep
Proof state before:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ (S', s') ⟹ t
Tactic:
apply ih
Proof state after:
no goals
Theorem: LoVe.abcd_bd
Proof state before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d
Tactic:
intro_and
Proof state after:
case left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b

case right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ d
Theorem: LoVe.abcd_bd
Proof state before:
case left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b

case right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ d
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.abcd_bd
Proof state before:
case right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ d
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.abcd_bacb
Proof state before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ a ∧ c ∧ b
Tactic:
intro_and
Proof state after:
case left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b

case right.left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ a

case right.right.left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ c

case right.right.right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b
Theorem: LoVe.abcd_bacb
Proof state before:
case left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b

case right.left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ a

case right.right.left
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ c

case right.right.right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b
Tactic:
repeat' sorry
Proof state after:
no goals
Theorem: LoVe.abcd_bacb
Proof state before:
case right.right.right
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.abcd_bd_again
Proof state before:
a b c d : Prop
⊢ a ∧ (b ∧ c) ∧ d → b ∧ d
Tactic:
intro h
Proof state after:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d
Theorem: LoVe.abcd_bd_again
Proof state before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d
Tactic:
cases_and
Proof state after:
case intro.intro.intro
a b c d : Prop
left : a
right : d
left_1 : b
right_1 : c
⊢ b ∧ d
Theorem: LoVe.abcd_bd_again
Proof state before:
case intro.intro.intro
a b c d : Prop
left : a
right : d
left_1 : b
right_1 : c
⊢ b ∧ d
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.abcd_bd_over_again
Proof state before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ d
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.abcd_bacb_again
Proof state before:
a b c d : Prop
h : a ∧ (b ∧ c) ∧ d
⊢ b ∧ a ∧ c ∧ b
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.abd_bacb_again
Proof state before:
a b c d : Prop
h : a ∧ b ∧ d
⊢ b ∧ a ∧ c ∧ b
Tactic:
destro_and
Proof state after:
case intro.intro.right.right.left
a b c d : Prop
left : a
left_1 : b
right : d
⊢ c
Theorem: LoVe.abd_bacb_again
Proof state before:
case intro.intro.right.right.left
a b c d : Prop
left : a
left_1 : b
right : d
⊢ c
Tactic:
sorry
Proof state after:
no goals
Theorem: LoVe.ab
Proof state before:
a b : Prop
h : a ∨ b
⊢ a ∨ b
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.abcdef_1
Proof state before:
a b c d e f : Prop
h : a ∧ b ∧ c ∧ d ∧ e ∧ f
⊢ f ∧ e ∧ f ∧ a ∧ d ∧ b ∧ c ∧ a
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.abcdef_2
Proof state before:
a b c d e f : Prop
h : a ∧ (b ∧ (c ∧ d) ∧ e) ∧ f
⊢ f ∧ e ∧ f ∧ a ∧ d ∧ b ∧ c ∧ a
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.abcdef_3
Proof state before:
a b c d e f : Prop
h : a ∧ b ∧ c ∧ d ∧ e ∧ f
⊢ f ∧ e ∧ f ∧ a ∧ d ∧ b ∧ c ∧ a
Tactic:
destro_and
Proof state after:
no goals
Theorem: LoVe.List.a_property_of_reverse
Proof state before:
α : Type
xs : List α
a : α
⊢ List.reverse (List.concat xs a) = a :: List.reverse xs
Tactic:
apply List.reverse_concat
Proof state after:
no goals
Theorem: LoVe.Fraction.ext
Proof state before:
a b : Fraction
hnum : a.num = b.num
hdenom : a.denom = b.denom
⊢ a = b
Tactic:
cases a with
| mk na da =>
  cases b with
  | mk nb db =>
    simp at *
    exact And.intro hnum hdenom
Proof state after:
no goals
Theorem: LoVe.Fraction.ext
Proof state before:
case mk
b : Fraction
na da : ℤ
denom_Neq_zero✝ : da ≠ 0
hnum : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.num = b.num
hdenom : { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ }.denom = b.denom
⊢ { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝ } = b
Tactic:
cases b with
| mk nb db =>
  simp at *
  exact And.intro hnum hdenom
Proof state after:
no goals
Theorem: LoVe.Fraction.ext
Proof state before:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum :
  { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ }.num =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }.num
hdenom :
  { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ }.denom =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }.denom
⊢ { num := na, denom := da, denom_Neq_zero := denom_Neq_zero✝¹ } =
    { num := nb, denom := db, denom_Neq_zero := denom_Neq_zero✝ }
Tactic:
simp at *
Proof state after:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum : na = nb
hdenom : da = db
⊢ na = nb ∧ da = db
Theorem: LoVe.Fraction.ext
Proof state before:
case mk.mk
na da : ℤ
denom_Neq_zero✝¹ : da ≠ 0
nb db : ℤ
denom_Neq_zero✝ : db ≠ 0
hnum : na = nb
hdenom : da = db
⊢ na = nb ∧ da = db
Tactic:
exact And.intro hnum hdenom
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.square_square
Proof state before:
a b c : ℕ
⊢ (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2 → a ^ 4 + b ^ 4 = c ^ 4
Tactic:
intro h
Proof state after:
a b c : ℕ
h : (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 4
Theorem: LoVe.BackwardProofs.square_square
Proof state before:
a b c : ℕ
h : (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 4
Tactic:
rw [←pow_mul, ←pow_mul, ←pow_mul] at h
Proof state after:
a b c : ℕ
h : a ^ (2 * 2) + b ^ (2 * 2) = c ^ (2 * 2)
⊢ a ^ 4 + b ^ 4 = c ^ 4
Theorem: LoVe.BackwardProofs.square_square
Proof state before:
a b c : ℕ
h : a ^ (2 * 2) + b ^ (2 * 2) = c ^ (2 * 2)
⊢ a ^ 4 + b ^ 4 = c ^ 4
Tactic:
exact h
Proof state after:
no goals
Theorem: LoVe.ring_example
Proof state before:
a b : Int2
⊢ (a + b) ^ 3 = a ^ 3 + 3 * a ^ 2 * b + 3 * a * b ^ 2 + b ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: LoVe.neg_mul_neg_Nat
Proof state before:
n : ℕ
z : ℤ
⊢ -z * -↑n = z * ↑n
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.neg_Nat_mul_neg
Proof state before:
n : ℕ
z : ℤ
⊢ -↑n * -z = ↑n * z
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Eq_coe_int_imp_Eq_Nat
Proof state before:
m n : ℕ
h : ↑m = ↑n
⊢ m = n
Tactic:
norm_cast at h
Proof state after:
no goals
Theorem: LoVe.Nat_coe_Int_add_eq_add_Nat_coe_Int
Proof state before:
m n : ℕ
⊢ ↑m + ↑n = ↑(m + n)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: LoVe.List_duplicates_example
Proof state before:
⊢ [2, 3, 3, 4] ≠ [2, 3, 4]
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.List_order_example
Proof state before:
⊢ [4, 3, 2] ≠ [2, 3, 4]
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.Multiset_duplicates_example
Proof state before:
⊢ {2, 3, 3, 4} ≠ {2, 3, 4}
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.Multiset_order_example
Proof state before:
⊢ {2, 3, 4} = {4, 3, 2}
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.Finset_duplicates_example
Proof state before:
⊢ {2, 3, 3, 4} = {2, 3, 4}
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.Finset_order_example
Proof state before:
⊢ {2, 3, 4} = {4, 3, 2}
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.list.length.Preorder_example
Proof state before:
⊢ [1] > []
Tactic:
decide
Proof state after:
no goals
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ (a + b) * (a + b) = a * (a + b) + b * (a + b)
Tactic:
simp only [add_mul, mul_add]
Proof state after:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
Tactic:
simp only [add_mul, mul_add]
Proof state after:
a b : ℕ
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
Tactic:
simp only [mul_comm]
Proof state after:
no goals
Theorem: LoVe.binomial_square
Proof state before:
a b : ℕ
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Tactic:
simp only [Nat.two_mul, add_mul, add_assoc]
Proof state after:
no goals
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
⊢ (a + b) * (a + b) = a * (a + b) + b * (a + b)
Tactic:
simp only [add_mul, mul_add]
Proof state after:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
⊢ a * a + b * a + (a * b + b * b) = a * a + a * b + (b * a + b * b)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
⊢ a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
Tactic:
simp only [add_mul, mul_add]
Proof state after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
⊢ a * a + a * b + (b * a + b * b) = a * a + a * b + b * a + b * b
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
⊢ a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
Tactic:
simp only [mul_comm]
Proof state after:
no goals
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Tactic:
simp only [Nat.two_mul, add_mul, add_assoc]
Proof state after:
no goals
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b
Tactic:
rw [h1]
Proof state after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * (a + b) + b * (a + b) = a * a + 2 * a * b + b * b
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * (a + b) + b * (a + b) = a * a + 2 * a * b + b * b
Tactic:
rw [h2]
Proof state after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + b * a + b * b = a * a + 2 * a * b + b * b
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + b * a + b * b = a * a + 2 * a * b + b * b
Tactic:
rw [h3]
Proof state after:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Theorem: LoVe.binomial_square₂
Proof state before:
a b : ℕ
h1 : (a + b) * (a + b) = a * (a + b) + b * (a + b)
h2 : a * (a + b) + b * (a + b) = a * a + a * b + b * a + b * b
h3 : a * a + a * b + b * a + b * b = a * a + a * b + a * b + b * b
h4 : a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
⊢ a * a + a * b + a * b + b * b = a * a + 2 * a * b + b * b
Tactic:
rw [h4]
Proof state after:
no goals
Theorem: LoVe.All.proof_of_False
Proof state before:
⊢ False
Tactic:
have hwrong : (∀x, x = 0 ∧ True) ↔ True :=
  All.one_point_wrong 0 (fun _ ↦ True)
Proof state after:
hwrong : (∀ (x : ℕ), x = 0 ∧ True) ↔ True
⊢ False
Theorem: LoVe.All.proof_of_False
Proof state before:
hwrong : (∀ (x : ℕ), x = 0 ∧ True) ↔ True
⊢ False
Tactic:
simp at hwrong
Proof state after:
hwrong : ∀ (x : ℕ), x = 0
⊢ False
Theorem: LoVe.All.proof_of_False
Proof state before:
hwrong : ∀ (x : ℕ), x = 0
⊢ False
Tactic:
have hone_eq_zero : 1 = 0 :=
  hwrong 1
Proof state after:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False
Theorem: LoVe.All.proof_of_False
Proof state before:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False
Tactic:
cases hone_eq_zero
Proof state after:
no goals
Theorem: LoVe.Exists.proof_of_False
Proof state before:
⊢ False
Tactic:
have hwrong : (∃x, x ≠ 0) ↔ False :=
  Exists.one_point_wrong 0 (fun _ ↦ False)
Proof state after:
hwrong : (∃ x, x ≠ 0) ↔ False
⊢ False
Theorem: LoVe.Exists.proof_of_False
Proof state before:
hwrong : (∃ x, x ≠ 0) ↔ False
⊢ False
Tactic:
simp at hwrong
Proof state after:
hwrong : ∀ (x : ℕ), x = 0
⊢ False
Theorem: LoVe.Exists.proof_of_False
Proof state before:
hwrong : ∀ (x : ℕ), x = 0
⊢ False
Tactic:
have hone_eq_zero : 1 = 0 :=
  hwrong 1
Proof state after:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False
Theorem: LoVe.Exists.proof_of_False
Proof state before:
hwrong : ∀ (x : ℕ), x = 0
hone_eq_zero : 1 = 0
⊢ False
Tactic:
cases hone_eq_zero
Proof state after:
no goals
Theorem: LoVe.Odd_1
Proof state before:
⊢ Odd 1
Tactic:
intro ho1
Proof state after:
ho1 : Even 1
⊢ False
Theorem: LoVe.Odd_1
Proof state before:
ho1 : Even 1
⊢ False
Tactic:
cases ho1
Proof state after:
no goals
Theorem: LoVe.Odd_3
Proof state before:
⊢ Odd 3
Tactic:
intro ho3
Proof state after:
ho3 : Even 3
⊢ False
Theorem: LoVe.Odd_3
Proof state before:
ho3 : Even 3
⊢ False
Tactic:
cases ho3 with
| add_two _ ho1 =>
  cases ho1
Proof state after:
no goals
Theorem: LoVe.Odd_3
Proof state before:
case add_two
ho1 : Even 1
⊢ False
Tactic:
cases ho1
Proof state after:
no goals
Theorem: LoVe.odd_5
Proof state before:
⊢ Odd 5
Tactic:
intro ho5
Proof state after:
ho5 : Even 5
⊢ False
Theorem: LoVe.odd_5
Proof state before:
ho5 : Even 5
⊢ False
Tactic:
cases ho5 with
| add_two _ ho3 =>
  cases ho3 with
  | add_two _ ho1 =>
    cases ho1
Proof state after:
no goals
Theorem: LoVe.odd_5
Proof state before:
case add_two
ho3 : Even 3
⊢ False
Tactic:
cases ho3 with
| add_two _ ho1 =>
  cases ho1
Proof state after:
no goals
Theorem: LoVe.odd_5
Proof state before:
case add_two.add_two
ho1 : Even 1
⊢ False
Tactic:
cases ho1
Proof state after:
no goals
Theorem: LoVe.Even_two_times
Proof state before:
m : ℕ
⊢ Even (2 * (m + 1))
Tactic:
apply Even.add_two
Proof state after:
case a
m : ℕ
⊢ Even (Nat.mul 2 (Nat.add m 0))
Theorem: LoVe.Even_two_times
Proof state before:
case a
m : ℕ
⊢ Even (Nat.mul 2 (Nat.add m 0))
Tactic:
simp
Proof state after:
case a
m : ℕ
⊢ Even (2 * m)
Theorem: LoVe.Even_two_times
Proof state before:
case a
m : ℕ
⊢ Even (2 * m)
Tactic:
apply Even_two_times
Proof state after:
no goals
Theorem: LoVe.not_ServAhead_advRecv
Proof state before:
⊢ ¬ServAhead Score.advRecv
Tactic:
intro h
Proof state after:
h : ServAhead Score.advRecv
⊢ False
Theorem: LoVe.not_ServAhead_advRecv
Proof state before:
h : ServAhead Score.advRecv
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: LoVe.not_ServAhead_gameRecv
Proof state before:
⊢ ¬ServAhead Score.gameRecv
Tactic:
intro h
Proof state after:
h : ServAhead Score.gameRecv
⊢ False
Theorem: LoVe.not_ServAhead_gameRecv
Proof state before:
h : ServAhead Score.gameRecv
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: LoVe.mirror_IsFull
Proof state before:
α : Type
⊢ ∀ (t : BTree α), IsFull (mirror t) → IsFull t
Tactic:
intro t fmt
Proof state after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
⊢ IsFull t
Theorem: LoVe.mirror_IsFull
Proof state before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
⊢ IsFull t
Tactic:
have fmmt : IsFull (mirror (mirror t)) :=
  IsFull_mirror _ fmt
Proof state after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull (mirror (mirror t))
⊢ IsFull t
Theorem: LoVe.mirror_IsFull
Proof state before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull (mirror (mirror t))
⊢ IsFull t
Tactic:
rw [mirror_mirror] at fmmt
Proof state after:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull t
⊢ IsFull t
Theorem: LoVe.mirror_IsFull
Proof state before:
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull t
⊢ IsFull t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BTree.map_eq_empty_iff
Proof state before:
α β : Type
f : α → β
⊢ map f empty = empty ↔ empty = empty
Tactic:
simp [BTree.map]
Proof state after:
no goals
Theorem: LoVe.BTree.map_eq_empty_iff
Proof state before:
α β : Type
f : α → β
a✝² : α
a✝¹ a✝ : BTree α
⊢ map f (node a✝² a✝¹ a✝) = empty ↔ node a✝² a✝¹ a✝ = empty
Tactic:
simp [BTree.map]
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
α β : Type
f : α → β
⊢ ∀ (t : BTree α), IsFull t → IsFull (map f t)
Tactic:
intro t hfull
Proof state after:
α β : Type
f : α → β
t : BTree α
hfull : IsFull t
⊢ IsFull (map f t)
Theorem: LoVe.BTree.map_mirror
Proof state before:
α β : Type
f : α → β
t : BTree α
hfull : IsFull t
⊢ IsFull (map f t)
Tactic:
induction hfull with
| empty =>
  simp [BTree.map]
  exact IsFull.empty
| node a l r hl hr hiff ihl ihr =>
  simp [BTree.map]
  apply IsFull.node
  { exact ihl }
  { exact ihr }
  { simp [BTree.map_eq_empty_iff]
    assumption }
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull (map f empty)
Tactic:
simp [BTree.map]
Proof state after:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull empty
Theorem: LoVe.BTree.map_mirror
Proof state before:
case empty
α β : Type
f : α → β
t : BTree α
⊢ IsFull empty
Tactic:
exact IsFull.empty
Proof state after:
no goals
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f (node a l r))
Tactic:
simp [BTree.map]
Proof state after:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (node (f a) (map f l) (map f r))
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (node (f a) (map f l) (map f r))
Tactic:
apply IsFull.node
Proof state after:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)

case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Theorem: LoVe.BTree.map_mirror
Proof state before:
case node.hl
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f l)

case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty
Tactic:
{ exact ihl }
Proof state after:
case node.hr
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f r)

case node.hiff
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ map f l = empty ↔ map f r = empty