internlm/Lean-Github huggingface dataset:
Theorem: rot_add_assoc
Proof state before:
⊢ ∀ (a b c : Rotation), a + b + c = a + (b + c)
Tactic:
intros a b c
Proof state after:
a b c : Rotation
⊢ a + b + c = a + (b + c)
Theorem: rot_add_assoc
Proof state before:
a b c : Rotation
⊢ a + b + c = a + (b + c)
Tactic:
cases a
Proof state after:
case r0
b c : Rotation
⊢ r0 + b + c = r0 + (b + c)

case r120
b c : Rotation
⊢ r120 + b + c = r120 + (b + c)

case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)
Theorem: rot_add_assoc
Proof state before:
case r0
b c : Rotation
⊢ r0 + b + c = r0 + (b + c)

case r120
b c : Rotation
⊢ r120 + b + c = r120 + (b + c)

case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)
Tactic:
repeat {
  cases b
  repeat {
   cases c
   repeat { rfl }
  }
}
Proof state after:
no goals
Theorem: rot_add_assoc
Proof state before:
case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)
Tactic:
cases b
Proof state after:
case r240.r0
c : Rotation
⊢ r240 + r0 + c = r240 + (r0 + c)

case r240.r120
c : Rotation
⊢ r240 + r120 + c = r240 + (r120 + c)

case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
Theorem: rot_add_assoc
Proof state before:
case r240.r0
c : Rotation
⊢ r240 + r0 + c = r240 + (r0 + c)

case r240.r120
c : Rotation
⊢ r240 + r120 + c = r240 + (r120 + c)

case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
Tactic:
repeat {
 cases c
 repeat { rfl }
}
Proof state after:
no goals
Theorem: rot_add_assoc
Proof state before:
case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
Tactic:
cases c
Proof state after:
case r240.r240.r0

⊢ r240 + r240 + r0 = r240 + (r240 + r0)

case r240.r240.r120

⊢ r240 + r240 + r120 = r240 + (r240 + r120)

case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)
Theorem: rot_add_assoc
Proof state before:
case r240.r240.r0

⊢ r240 + r240 + r0 = r240 + (r240 + r0)

case r240.r240.r120

⊢ r240 + r240 + r120 = r240 + (r240 + r120)

case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_add_assoc
Proof state before:
case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_zero_add
Proof state before:
⊢ ∀ (a : Rotation), 0 + a = a
Tactic:
intro a
Proof state after:
a : Rotation
⊢ 0 + a = a
Theorem: rot_zero_add
Proof state before:
a : Rotation
⊢ 0 + a = a
Tactic:
cases a
Proof state after:
case r0

⊢ 0 + r0 = r0

case r120

⊢ 0 + r120 = r120

case r240

⊢ 0 + r240 = r240
Theorem: rot_zero_add
Proof state before:
case r0

⊢ 0 + r0 = r0

case r120

⊢ 0 + r120 = r120

case r240

⊢ 0 + r240 = r240
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_zero_add
Proof state before:
case r240

⊢ 0 + r240 = r240
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_add_zero
Proof state before:
⊢ ∀ (a : Rotation), a + 0 = a
Tactic:
intro a
Proof state after:
a : Rotation
⊢ a + 0 = a
Theorem: rot_add_zero
Proof state before:
a : Rotation
⊢ a + 0 = a
Tactic:
cases a
Proof state after:
case r0

⊢ r0 + 0 = r0

case r120

⊢ r120 + 0 = r120

case r240

⊢ r240 + 0 = r240
Theorem: rot_add_zero
Proof state before:
case r0

⊢ r0 + 0 = r0

case r120

⊢ r120 + 0 = r120

case r240

⊢ r240 + 0 = r240
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_add_zero
Proof state before:
case r240

⊢ r240 + 0 = r240
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_zero_vadd
Proof state before:
⊢ ∀ (p : State), 0 +ᵥ p = p
Tactic:
intro p
Proof state after:
p : State
⊢ 0 +ᵥ p = p
Theorem: rot_zero_vadd
Proof state before:
p : State
⊢ 0 +ᵥ p = p
Tactic:
cases p
Proof state after:
case heading
h✝ : K
unit✝ : ℕ
⊢ 0 +ᵥ heading h✝ unit✝ = heading h✝ unit✝
Theorem: rot_zero_vadd
Proof state before:
case heading
h✝ : K
unit✝ : ℕ
⊢ 0 +ᵥ heading h✝ unit✝ = heading h✝ unit✝
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_zero_vadd
Proof state before:
case heading
h✝ : K
unit✝ : ℕ
⊢ 0 +ᵥ heading h✝ unit✝ = heading h✝ unit✝
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
⊢ ∀ (g₁ g₂ : Rotation) (p : State), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Tactic:
intros g₁ g₂ p
Proof state after:
g₁ g₂ : Rotation
p : State
⊢ g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
g₁ g₂ : Rotation
p : State
⊢ g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Tactic:
cases g₁
Proof state after:
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Tactic:
repeat {
  cases g₂
  repeat {
    cases p
    repeat rfl
  }
}
Proof state after:
case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)
Tactic:
cases g₂
Proof state after:
case r120.r0
p : State
⊢ r120 + r0 +ᵥ p = r120 +ᵥ (r0 +ᵥ p)

case r120.r120
p : State
⊢ r120 + r120 +ᵥ p = r120 +ᵥ (r120 +ᵥ p)

case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
case r120.r0
p : State
⊢ r120 + r0 +ᵥ p = r120 +ᵥ (r0 +ᵥ p)

case r120.r120
p : State
⊢ r120 + r120 +ᵥ p = r120 +ᵥ (r120 +ᵥ p)

case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Tactic:
repeat {
  cases p
  repeat rfl
}
Proof state after:
case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Tactic:
cases p
Proof state after:
case r120.r240.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r240 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r240 +ᵥ heading h✝ unit✝)
Theorem: rot_add_vadd
Proof state before:
case r120.r120.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r120 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r120 +ᵥ heading h✝ unit✝)
Tactic:
repeat rfl
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
case r120.r120.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r120 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r120 +ᵥ heading h✝ unit✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_add_neg_left
Proof state before:
⊢ ∀ (a : Rotation), -a + a = 0
Tactic:
intro a
Proof state after:
a : Rotation
⊢ -a + a = 0
Theorem: rot_add_neg_left
Proof state before:
a : Rotation
⊢ -a + a = 0
Tactic:
cases a
Proof state after:
case r0

⊢ -r0 + r0 = 0

case r120

⊢ -r120 + r120 = 0

case r240

⊢ -r240 + r240 = 0
Theorem: rot_add_neg_left
Proof state before:
case r0

⊢ -r0 + r0 = 0

case r120

⊢ -r120 + r120 = 0

case r240

⊢ -r240 + r240 = 0
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_add_neg_left
Proof state before:
case r240

⊢ -r240 + r240 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_state_vsub_vadd'
Proof state before:
⊢ ∀ (p1 p2 : State), p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
intro p1 p2
Proof state after:
p1 p2 : State
⊢ p1 -ᵥ p2 +ᵥ p2 = p1
Theorem: rot_state_vsub_vadd'
Proof state before:
p1 p2 : State
⊢ p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
cases p1
Proof state after:
case heading
p2 : State
h✝ : K
unit✝ : ℕ
⊢ heading h✝ unit✝ -ᵥ p2 +ᵥ p2 = heading h✝ unit✝
Theorem: rot_state_vsub_vadd'
Proof state before:
case heading
p2 : State
h✝ : K
unit✝ : ℕ
⊢ heading h✝ unit✝ -ᵥ p2 +ᵥ p2 = heading h✝ unit✝
Tactic:
cases p2
Proof state after:
case heading.heading
h✝¹ : K
unit✝¹ : ℕ
h✝ : K
unit✝ : ℕ
⊢ heading h✝¹ unit✝¹ -ᵥ heading h✝ unit✝ +ᵥ heading h✝ unit✝ = heading h✝¹ unit✝¹
Theorem: rot_state_vadd_vsub'
Proof state before:
⊢ ∀ (g : Rotation) (p : State), g +ᵥ p -ᵥ p = g
Tactic:
intros g p
Proof state after:
g : Rotation
p : State
⊢ g +ᵥ p -ᵥ p = g
Theorem: rot_state_vadd_vsub'
Proof state before:
g : Rotation
p : State
⊢ g +ᵥ p -ᵥ p = g
Tactic:
cases g
Proof state after:
case r0
p : State
⊢ r0 +ᵥ p -ᵥ p = r0

case r120
p : State
⊢ r120 +ᵥ p -ᵥ p = r120

case r240
p : State
⊢ r240 +ᵥ p -ᵥ p = r240
Theorem: rot_state_vadd_vsub'
Proof state before:
case r0
p : State
⊢ r0 +ᵥ p -ᵥ p = r0
Tactic:
cases p
Proof state after:
case r0.heading
h✝ : K
unit✝ : ℕ
⊢ r0 +ᵥ heading h✝ unit✝ -ᵥ heading h✝ unit✝ = r0
Theorem: eq_nat_is_refl
Proof state before:
⊢ Reflexive Eq
Tactic:
unfold Reflexive
Proof state after:
⊢ ∀ (x : ℕ), x = x
Theorem: eq_nat_is_refl
Proof state before:
⊢ ∀ (x : ℕ), x = x
Tactic:
intro x
Proof state after:
x : ℕ
⊢ x = x
Theorem: eq_nat_is_refl
Proof state before:
x : ℕ
⊢ x = x
Tactic:
exact rfl
Proof state after:
no goals
Theorem: eq_nat_is_symm
Proof state before:
⊢ Symmetric Eq
Tactic:
unfold Symmetric
Proof state after:
⊢ ∀ ⦃x y : ℕ⦄, x = y → y = x
Theorem: eq_nat_is_symm
Proof state before:
⊢ ∀ ⦃x y : ℕ⦄, x = y → y = x
Tactic:
intro x y
Proof state after:
x y : ℕ
⊢ x = y → y = x
Theorem: eq_nat_is_symm
Proof state before:
x y : ℕ
⊢ x = y → y = x
Tactic:
intro hxy
Proof state after:
x y : ℕ
hxy : x = y
⊢ y = x
Theorem: eq_nat_is_symm
Proof state before:
x y : ℕ
hxy : x = y
⊢ y = x
Tactic:
rw [hxy]
Proof state after:
no goals
Theorem: eq_nat_is_trans
Proof state before:
⊢ Transitive Eq
Tactic:
unfold Transitive
Proof state after:
⊢ ∀ ⦃x y z : ℕ⦄, x = y → y = z → x = z
Theorem: eq_nat_is_trans
Proof state before:
⊢ ∀ ⦃x y z : ℕ⦄, x = y → y = z → x = z
Tactic:
intros x y z
Proof state after:
x y z : ℕ
⊢ x = y → y = z → x = z
Theorem: eq_nat_is_trans
Proof state before:
x y z : ℕ
⊢ x = y → y = z → x = z
Tactic:
intros hxy hyz
Proof state after:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z
Theorem: eq_nat_is_trans
Proof state before:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z
Tactic:
rw [hxy]
Proof state after:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ y = z
Theorem: eq_nat_is_trans
Proof state before:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ y = z
Tactic:
rw [hyz]
Proof state after:
no goals
Theorem: cong_mod_n_equiv'
Proof state before:
⊢ ∀ (n : ℕ), Equivalence (cong_mod_n n)
Tactic:
intro n
Proof state after:
n : ℕ
⊢ Equivalence (cong_mod_n n)
Theorem: cong_mod_n_rfl
Proof state before:
⊢ ∀ (n : ℕ), Reflexive (cong_mod_n n)
Tactic:
intro n
Proof state after:
n : ℕ
⊢ Reflexive (cong_mod_n n)
Theorem: cong_mod_n_rfl
Proof state before:
n : ℕ
⊢ Reflexive (cong_mod_n n)
Tactic:
unfold cong_mod_n
Proof state after:
n : ℕ
⊢ Reflexive fun a b => a % n = b % n
Theorem: cong_mod_n_rfl
Proof state before:
n : ℕ
⊢ Reflexive fun a b => a % n = b % n
Tactic:
unfold Reflexive
Proof state after:
n : ℕ
⊢ ∀ (x : ℕ), (fun a b => a % n = b % n) x x
Theorem: cong_mod_n_rfl
Proof state before:
n : ℕ
⊢ ∀ (x : ℕ), (fun a b => a % n = b % n) x x
Tactic:
intro a
Proof state after:
n a : ℕ
⊢ a % n = a % n
Theorem: cong_mod_n_rfl
Proof state before:
n a : ℕ
⊢ a % n = a % n
Tactic:
exact rfl
Proof state after:
no goals
Theorem: cong_mod_n_symm
Proof state before:
⊢ ∀ (n : ℕ), Symmetric (cong_mod_n n)
Tactic:
intro n
Proof state after:
n : ℕ
⊢ Symmetric (cong_mod_n n)
Theorem: cong_mod_n_symm
Proof state before:
n : ℕ
⊢ Symmetric (cong_mod_n n)
Tactic:
unfold Symmetric
Proof state after:
n : ℕ
⊢ ∀ ⦃x y : ℕ⦄, cong_mod_n n x y → cong_mod_n n y x
Theorem: cong_mod_n_symm
Proof state before:
n : ℕ
⊢ ∀ ⦃x y : ℕ⦄, cong_mod_n n x y → cong_mod_n n y x
Tactic:
intros x y
Proof state after:
n x y : ℕ
⊢ cong_mod_n n x y → cong_mod_n n y x
Theorem: cong_mod_n_symm
Proof state before:
n x y : ℕ
⊢ cong_mod_n n x y → cong_mod_n n y x
Tactic:
intro hxy
Proof state after:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ cong_mod_n n y x
Theorem: cong_mod_n_symm
Proof state before:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ cong_mod_n n y x
Tactic:
unfold cong_mod_n
Proof state after:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ y % n = x % n
Theorem: cong_mod_n_symm
Proof state before:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ y % n = x % n
Tactic:
unfold cong_mod_n at hxy
Proof state after:
n x y : ℕ
hxy : x % n = y % n
⊢ y % n = x % n
Theorem: cong_mod_n_symm
Proof state before:
n x y : ℕ
hxy : x % n = y % n
⊢ y % n = x % n
Tactic:
rw [hxy]
Proof state after:
no goals
Theorem: cong_mod_trans
Proof state before:
⊢ ∀ (n : ℕ), Transitive (cong_mod_n n)
Tactic:
intro n a b c hab hbc
Proof state after:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ cong_mod_n n a c
Theorem: cong_mod_trans
Proof state before:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ cong_mod_n n a c
Tactic:
unfold cong_mod_n
Proof state after:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ a % n = c % n
Theorem: cong_mod_trans
Proof state before:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ a % n = c % n
Tactic:
unfold cong_mod_n at hab hbc
Proof state after:
n a b c : ℕ
hab : a % n = b % n
hbc : b % n = c % n
⊢ a % n = c % n
Theorem: cong_mod_trans
Proof state before:
n a b c : ℕ
hab : a % n = b % n
hbc : b % n = c % n
⊢ a % n = c % n
Tactic:
rw [hab, hbc]
Proof state after:
no goals
Theorem: cong_mod_n_equiv
Proof state before:
⊢ ∀ (n : ℕ), Equivalence (cong_mod_n n)
Tactic:
intro n
Proof state after:
n : ℕ
⊢ Equivalence (cong_mod_n n)
Theorem: cong_mod_n_equiv
Proof state before:
n : ℕ
⊢ Equivalence (cong_mod_n n)
Tactic:
unfold cong_mod_n
Proof state after:
n : ℕ
⊢ Equivalence fun a b => a % n = b % n
Theorem: cong_mod_n_equiv
Proof state before:
n : ℕ
⊢ Equivalence fun a b => a % n = b % n
Tactic:
exact Equivalence.mk 
  (by intro x; rfl)
  (by intros x y h; rw [h]) 
  (by intros x y z hxy hyz; rw [hxy, hyz])
Proof state after:
no goals
Theorem: cong_mod_n_equiv
Proof state before:
n : ℕ
⊢ ∀ (x : ℕ), x % n = x % n
Tactic:
intro x
Proof state after:
n x : ℕ
⊢ x % n = x % n
Theorem: cong_mod_n_equiv
Proof state before:
n x : ℕ
⊢ x % n = x % n
Tactic:
rfl
Proof state after:
no goals
Theorem: cong_mod_n_equiv
Proof state before:
n : ℕ
⊢ ∀ {x y : ℕ}, x % n = y % n → y % n = x % n
Tactic:
intros x y h
Proof state after:
n x y : ℕ
h : x % n = y % n
⊢ y % n = x % n
Theorem: cong_mod_n_equiv
Proof state before:
n x y : ℕ
h : x % n = y % n
⊢ y % n = x % n
Tactic:
rw [h]
Proof state after:
no goals
Theorem: cong_mod_n_equiv
Proof state before:
n : ℕ
⊢ ∀ {x y z : ℕ}, x % n = y % n → y % n = z % n → x % n = z % n
Tactic:
intros x y z hxy hyz
Proof state after:
n x y z : ℕ
hxy : x % n = y % n
hyz : y % n = z % n
⊢ x % n = z % n
Theorem: cong_mod_n_equiv
Proof state before:
n x y z : ℕ
hxy : x % n = y % n
hyz : y % n = z % n
⊢ x % n = z % n
Tactic:
rw [hxy, hyz]
Proof state after:
no goals
Theorem: succ_inj
Proof state before:
⊢ Injective fun n => n + 1
Tactic:
unfold Injective
Proof state after:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, (fun n => n + 1) a₁ = (fun n => n + 1) a₂ → a₁ = a₂
Theorem: succ_inj
Proof state before:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, (fun n => n + 1) a₁ = (fun n => n + 1) a₂ → a₁ = a₂
Tactic:
intros a1 a2 h
Proof state after:
a1 a2 : ℕ
h : (fun n => n + 1) a1 = (fun n => n + 1) a2
⊢ a1 = a2
Theorem: succ_inj
Proof state before:
a1 a2 : ℕ
h : (fun n => n + 1) a1 = (fun n => n + 1) a2
⊢ a1 = a2
Tactic:
simp [Nat.add] at h
Proof state after:
a1 a2 : ℕ
h : a1 = a2
⊢ a1 = a2
Theorem: succ_inj
Proof state before:
a1 a2 : ℕ
h : a1 = a2
⊢ a1 = a2
Tactic:
assumption
Proof state after:
no goals
Theorem: not_succ_surj
Proof state before:
⊢ ¬Surjective fun n => n + 1
Tactic:
unfold Surjective
Proof state after:
⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
Theorem: not_succ_surj
Proof state before:
⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
Tactic:
intro h
Proof state after:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
⊢ False
Theorem: not_succ_surj
Proof state before:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
⊢ False
Tactic:
let contra := h 0
Proof state after:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
contra : ∃ a, (fun n => n + 1) a = 0 := h 0
⊢ False
Theorem: not_succ_surj
Proof state before:
h : ∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b
contra : ∃ a, (fun n => n + 1) a = 0 := h 0
⊢ False
Tactic:
simp [Nat.add] at contra
Proof state after:
no goals
Theorem: inj_not
Proof state before:
⊢ Injective Bool.not
Tactic:
unfold Injective
Proof state after:
⊢ ∀ ⦃a₁ a₂ : Bool⦄, Bool.not a₁ = Bool.not a₂ → a₁ = a₂
Theorem: inj_not
Proof state before:
⊢ ∀ ⦃a₁ a₂ : Bool⦄, Bool.not a₁ = Bool.not a₂ → a₁ = a₂
Tactic:
intros a1 a2 h
Proof state after:
a1 a2 : Bool
h : Bool.not a1 = Bool.not a2
⊢ a1 = a2
Theorem: inj_not
Proof state before:
a1 a2 : Bool
h : Bool.not a1 = Bool.not a2
⊢ a1 = a2
Tactic:
cases a1 with
  | true =>
      cases a2 with
      | true => rfl
      | false => nomatch h
  | false =>
        cases a2 with
        | true => nomatch h
        | false => rfl
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case true
a2 : Bool
h : Bool.not true = Bool.not a2
⊢ true = a2
Tactic:
cases a2 with
| true => rfl
| false => nomatch h
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case true.true
h : Bool.not true = Bool.not true
⊢ true = true
Tactic:
rfl
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case true.false
h : Bool.not true = Bool.not false
⊢ true = false
Tactic:
nomatch h
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case false
a2 : Bool
h : Bool.not false = Bool.not a2
⊢ false = a2
Tactic:
cases a2 with
| true => nomatch h
| false => rfl
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case false.true
h : Bool.not false = Bool.not true
⊢ false = true
Tactic:
nomatch h
Proof state after:
no goals
Theorem: inj_not
Proof state before:
case false.false
h : Bool.not false = Bool.not false
⊢ false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: surj_not
Proof state before:
⊢ Surjective Bool.not
Tactic:
unfold Surjective
Proof state after:
⊢ ∀ (b : Bool), ∃ a, Bool.not a = b
Theorem: surj_not
Proof state before:
⊢ ∀ (b : Bool), ∃ a, Bool.not a = b
Tactic:
intro b
Proof state after:
b : Bool
⊢ ∃ a, Bool.not a = b
Theorem: surj_not
Proof state before:
b : Bool
⊢ ∃ a, Bool.not a = b
Tactic:
cases b with 
| true => exact ⟨ false, rfl ⟩ 
| false => exact ⟨ true, rfl ⟩
Proof state after:
no goals
Theorem: surj_not
Proof state before:
case true

⊢ ∃ a, Bool.not a = true
Tactic:
exact ⟨ false, rfl ⟩
Proof state after:
no goals
Theorem: surj_not
Proof state before:
case false

⊢ ∃ a, Bool.not a = false
Tactic:
exact ⟨ true, rfl ⟩
Proof state after:
no goals
Theorem: not_bij
Proof state before:
⊢ Bijective Bool.not
Tactic:
unfold Bijective
Proof state after:
⊢ Injective Bool.not ∧ Surjective Bool.not
Theorem: not_bij
Proof state before:
⊢ Injective Bool.not ∧ Surjective Bool.not
Tactic:
exact ⟨ inj_not, surj_not ⟩
Proof state after:
no goals
Theorem: rot_zero_vadd
Proof state before:
p : State
⊢ 0 +ᵥ p = p
Tactic:
cases p
Proof state after:
case s0

⊢ 0 +ᵥ s0 = s0

case s120

⊢ 0 +ᵥ s120 = s120

case s240

⊢ 0 +ᵥ s240 = s240
Theorem: rot_zero_vadd
Proof state before:
case s0

⊢ 0 +ᵥ s0 = s0

case s120

⊢ 0 +ᵥ s120 = s120

case s240

⊢ 0 +ᵥ s240 = s240
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_zero_vadd
Proof state before:
case s240

⊢ 0 +ᵥ s240 = s240
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Tactic:
repeat {
  cases g₂
  repeat {
    cases p
    repeat rfl
  }
}
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Tactic:
cases g₂
Proof state after:
case r240.r0
p : State
⊢ r240 + r0 +ᵥ p = r240 +ᵥ (r0 +ᵥ p)

case r240.r120
p : State
⊢ r240 + r120 +ᵥ p = r240 +ᵥ (r120 +ᵥ p)

case r240.r240
p : State
⊢ r240 + r240 +ᵥ p = r240 +ᵥ (r240 +ᵥ p)
Theorem: rot_add_vadd
Proof state before:
case r240.r0
p : State
⊢ r240 + r0 +ᵥ p = r240 +ᵥ (r0 +ᵥ p)

case r240.r120
p : State
⊢ r240 + r120 +ᵥ p = r240 +ᵥ (r120 +ᵥ p)

case r240.r240
p : State
⊢ r240 + r240 +ᵥ p = r240 +ᵥ (r240 +ᵥ p)
Tactic:
repeat {
  cases p
  repeat rfl
}
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
case r240.r240
p : State
⊢ r240 + r240 +ᵥ p = r240 +ᵥ (r240 +ᵥ p)
Tactic:
cases p
Proof state after:
case r240.r240.s0

⊢ r240 + r240 +ᵥ s0 = r240 +ᵥ (r240 +ᵥ s0)

case r240.r240.s120

⊢ r240 + r240 +ᵥ s120 = r240 +ᵥ (r240 +ᵥ s120)

case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)
Theorem: rot_add_vadd
Proof state before:
case r240.r240.s0

⊢ r240 + r240 +ᵥ s0 = r240 +ᵥ (r240 +ᵥ s0)

case r240.r240.s120

⊢ r240 + r240 +ᵥ s120 = r240 +ᵥ (r240 +ᵥ s120)

case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)
Tactic:
repeat rfl
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_state_vsub_vadd'
Proof state before:
p1 p2 : State
⊢ p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
cases p1
Proof state after:
case s0
p2 : State
⊢ s0 -ᵥ p2 +ᵥ p2 = s0

case s120
p2 : State
⊢ s120 -ᵥ p2 +ᵥ p2 = s120

case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240
Theorem: rot_state_vsub_vadd'
Proof state before:
case s0
p2 : State
⊢ s0 -ᵥ p2 +ᵥ p2 = s0

case s120
p2 : State
⊢ s120 -ᵥ p2 +ᵥ p2 = s120

case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240
Tactic:
repeat { 
  cases p2 
  repeat rfl
}
Proof state after:
no goals
Theorem: rot_state_vsub_vadd'
Proof state before:
case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240
Tactic:
cases p2
Proof state after:
case s240.s0

⊢ s240 -ᵥ s0 +ᵥ s0 = s240

case s240.s120

⊢ s240 -ᵥ s120 +ᵥ s120 = s240

case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240
Theorem: rot_state_vsub_vadd'
Proof state before:
case s240.s0

⊢ s240 -ᵥ s0 +ᵥ s0 = s240

case s240.s120

⊢ s240 -ᵥ s120 +ᵥ s120 = s240

case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240
Tactic:
repeat rfl
Proof state after:
no goals
Theorem: rot_state_vsub_vadd'
Proof state before:
case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240
Tactic:
rfl
Proof state after:
no goals
Theorem: rot_state_vadd_vsub'
Proof state before:
case r0
p : State
⊢ r0 +ᵥ p -ᵥ p = r0

case r120
p : State
⊢ r120 +ᵥ p -ᵥ p = r120

case r240
p : State
⊢ r240 +ᵥ p -ᵥ p = r240
Tactic:
repeat {
  cases p
  repeat { rfl }
}
Proof state after:
no goals
Theorem: rot_state_vadd_vsub'
Proof state before:
case r240
p : State
⊢ r240 +ᵥ p -ᵥ p = r240
Tactic:
cases p
Proof state after:
case r240.s0

⊢ r240 +ᵥ s0 -ᵥ s0 = r240

case r240.s120

⊢ r240 +ᵥ s120 -ᵥ s120 = r240

case r240.s240

⊢ r240 +ᵥ s240 -ᵥ s240 = r240
Theorem: rot_state_vadd_vsub'
Proof state before:
case r240.s0

⊢ r240 +ᵥ s0 -ᵥ s0 = r240

case r240.s120

⊢ r240 +ᵥ s120 -ᵥ s120 = r240

case r240.s240

⊢ r240 +ᵥ s240 -ᵥ s240 = r240
Tactic:
repeat { rfl }
Proof state after:
no goals
Theorem: rot_state_vadd_vsub'
Proof state before:
case r240.s240

⊢ r240 +ᵥ s240 -ᵥ s240 = r240
Tactic:
rfl
Proof state after:
no goals
Theorem: cs2120f23.proof_equal
Proof state before:
⊢ Birds_chirping.boo = Birds_chirping.yep
Tactic:
trivial
Proof state after:
no goals
Theorem: eq_is_symm
Proof state before:
α : Type
a b : α
h : a = b
⊢ b = a
Tactic:
rw [h]
Proof state after:
no goals
Theorem: eq_rel_trans
Proof state before:
α : Type
a b c : α
ab : a = b
bc : b = c
⊢ a = c
Tactic:
rw [ab]
Proof state after:
α : Type
a b c : α
ab : a = b
bc : b = c
⊢ b = c
Theorem: eq_rel_trans
Proof state before:
α : Type
a b c : α
ab : a = b
bc : b = c
⊢ b = c
Tactic:
rw [bc]
Proof state after:
no goals
Theorem: rot_zero_add
Proof state before:
⊢ ∀ (a : Rotation), 0 + a = a
Tactic:
_
Proof state after:
no goals
Theorem: rot_add_zero
Proof state before:
⊢ ∀ (a : Rotation), a + 0 = a
Tactic:
_
Proof state after:
no goals
Theorem: rot_zero_vadd
Proof state before:
⊢ ∀ (p : State), 0 +ᵥ p = p
Tactic:
_
Proof state after:
no goals
Theorem: rot_add_vadd
Proof state before:
⊢ ∀ (g₁ g₂ : Rotation) (p : State), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Tactic:
_
Proof state after:
no goals
Theorem: rot_add_neg_left
Proof state before:
⊢ ∀ (a : Rotation), -a + a = 0
Tactic:
_
Proof state after:
no goals
Theorem: rot_state_vsub_vadd'
Proof state before:
⊢ ∀ (p1 p2 : State), p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
_
Proof state after:
no goals
Theorem: rot_state_vadd_vsub'
Proof state before:
⊢ ∀ (g : Rotation) (p : State), g +ᵥ p -ᵥ p = g
Tactic:
_
Proof state after:
no goals