internlm/Lean-Github huggingface dataset:
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
. intros hx; exact ⟨x, hx, subset_rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f
Tactic:
intros hx
Proof state after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Tactic:
have ⟨t, ht⟩ := hx
Proof state after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
t : Set α
ht : t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
t : Set α
ht : t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Tactic:
exact superset_mem ht.1 ht.2
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
intros hx
Proof state after:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
hx : x ∈ f
⊢ ∃ t, t ∈ f ∧ t ⊆ x
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
hx : x ∈ f
⊢ ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
exact ⟨x, hx, subset_rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Basis.mem_as_filter_of_mem
Proof state before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ s ∈ as_filter b
Tactic:
sorry
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
α : Type u_1
f : Filter α
⊢ Basis.as_filter (as_basis f) = f
Tactic:
sorry
Proof state after:
no goals
Theorem: eq_zero_or_exists_succ
Proof state before:
n : ℕ
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
have hnzp : n = 0 ∨ n > 0 := Nat.eq_zero_or_pos n
Proof state after:
n : ℕ
hnzp : n = 0 ∨ n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
n : ℕ
hnzp : n = 0 ∨ n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
eliminate hnzp
Proof state after:
case inl
n : ℕ
h✝ : n = 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1

case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
case inl
n : ℕ
h✝ : n = 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1

case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
{left; assumption}
Proof state after:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
{
  right
  eliminate (Nat.exists_eq_succ_of_ne_zero (by linarith)) with w
  existsi w
  assumption
}
Proof state after:
no goals
Theorem: eq_zero_or_exists_succ
Proof state before:
case inl
n : ℕ
h✝ : n = 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
left
Proof state after:
case inl.h
n : ℕ
h✝ : n = 0
⊢ n = 0
Theorem: eq_zero_or_exists_succ
Proof state before:
case inl.h
n : ℕ
h✝ : n = 0
⊢ n = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: eq_zero_or_exists_succ
Proof state before:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
right
Proof state after:
case inr.h
n : ℕ
h✝ : n > 0
⊢ ∃ n0, n = n0 + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
case inr.h
n : ℕ
h✝ : n > 0
⊢ ∃ n0, n = n0 + 1
Tactic:
eliminate (Nat.exists_eq_succ_of_ne_zero (by linarith)) with w
Proof state after:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ ∃ n0, n = n0 + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ ∃ n0, n = n0 + 1
Tactic:
existsi w
Proof state after:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ n = w + 1
Theorem: eq_zero_or_exists_succ
Proof state before:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ n = w + 1
Tactic:
assumption
Proof state after:
no goals
Theorem: eq_zero_or_exists_succ
Proof state before:
n : ℕ
h✝ : n > 0
⊢ ?m.18553 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: exists_succ_of_gt
Proof state before:
x n : ℕ
⊢ x < n → ∃ n0, n = n0 + 1
Tactic:
intro h
Proof state after:
x n : ℕ
h : x < n
⊢ ∃ n0, n = n0 + 1
Theorem: exists_succ_of_gt
Proof state before:
x n : ℕ
h : x < n
⊢ ∃ n0, n = n0 + 1
Tactic:
have hnzp : n = 0 ∨ ∃ n0, n = n0 + 1 := eq_zero_or_exists_succ n
Proof state after:
x n : ℕ
h : x < n
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Theorem: exists_succ_of_gt
Proof state before:
x n : ℕ
h : x < n
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
eliminate hnzp
Proof state after:
case inl
x n : ℕ
h : x < n
h✝ : n = 0
⊢ ∃ n0, n = n0 + 1

case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Theorem: exists_succ_of_gt
Proof state before:
case inl
x n : ℕ
h : x < n
h✝ : n = 0
⊢ ∃ n0, n = n0 + 1

case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
linarith
Proof state after:
case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Theorem: exists_succ_of_gt
Proof state before:
case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
assumption
Proof state after:
no goals
Theorem: nat_eq_or_ne
Proof state before:
n k : ℕ
⊢ n = k ∨ n ≠ k
Tactic:
exact Decidable.eq_or_ne n k
Proof state after:
no goals
Theorem: eq_zero_or_ne_zero
Proof state before:
n : ℕ
⊢ n = 0 ∨ n ≠ 0
Tactic:
exact nat_eq_or_ne n 0
Proof state after:
no goals
Theorem: Choose_expansion_of_pos_n_k
Proof state before:
n k : ℕ
⊢ 0 < n → 0 < k → (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
intro hn hk
Proof state after:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Theorem: Choose_expansion_of_pos_n_k
Proof state before:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
rewrite [Nat.pos_iff_ne_zero] at *
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Theorem: Choose_expansion_of_pos_n_k
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = n¡ / (k¡ * (n - k)¡)
Tactic:
simp [Choose]
Proof state after:
no goals
Theorem: _112
Proof state before:
⊢ 1 + 1 = 2
Tactic:
numbers
Proof state after:
no goals
Theorem: _x112
Proof state before:
x : ℕ
⊢ x + 1 + 1 = x + 2
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: _x11x
Proof state before:
x : ℕ
⊢ x + 1 - 1 = x
Tactic:
simp
Proof state after:
no goals
Theorem: _011
Proof state before:
⊢ 0 + 1 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: _s01
Proof state before:
⊢ Nat.succ 0 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Choose_zero_eq_one
Proof state before:
⊢ ∀ (n : ℕ), (n C 0) = 1
Tactic:
simp [Choose]
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
n : ℕ
⊢ (n C 1) = n
Tactic:
have hnzp : n = 0 ∨ ∃ n0, n = n0 + 1 := eq_zero_or_exists_succ n
Proof state after:
n : ℕ
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Theorem: Choose_one_eq_self
Proof state before:
n : ℕ
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
eliminate hnzp with h h
Proof state after:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n

case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Theorem: Choose_one_eq_self
Proof state before:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n

case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
{simp [h]}
Proof state after:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Theorem: Choose_one_eq_self
Proof state before:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
{
  eliminate h with n0 h
  have : n ≠ 0 := by linarith 
  simp [Choose]
  rewrite [h, Nat.factorial_succ]
  simp
  rewrite [Nat.mul_div_cancel]
  {linarith}
  {apply Nat.factorial_pos}
}
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
eliminate h with n0 h
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
⊢ (n C 1) = n
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
⊢ (n C 1) = n
Tactic:
have : n ≠ 0 := by linarith
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n C 1) = n
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n C 1) = n
Tactic:
simp [Choose]
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n¡ / (n - 1)¡ = n
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n¡ / (n - 1)¡ = n
Tactic:
rewrite [h, Nat.factorial_succ]
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / (n0 + 1 - 1)¡ = n0 + 1
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / (n0 + 1 - 1)¡ = n0 + 1
Tactic:
simp
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / n0¡ = n0 + 1
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / n0¡ = n0 + 1
Tactic:
rewrite [Nat.mul_div_cancel]
Proof state after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1

case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1

case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
{linarith}
Proof state after:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
{apply Nat.factorial_pos}
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
n n0 : ℕ
h : n = n0 + 1
⊢ n ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Choose_one_eq_self
Proof state before:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
apply Nat.factorial_pos
Proof state after:
no goals
Theorem: Choose_self_eq_one
Proof state before:
n : ℕ
⊢ (n C n) = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
⊢ n ≠ 0 → k ≠ 0 → n - k ≠ 0 → (n C k) = (n C n - k)
Tactic:
intros hn hk hnk
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
simp [Choose]
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / (k¡ * (n - k)¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / (k¡ * (n - k)¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
Tactic:
rewrite [mul_comm]
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
Tactic:
rewrite [Nat.sub_sub_self]
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * k¡)

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * k¡)

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
{ reflexivity }
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
{ have : k < n
  { apply lt_of_not_le
    rewrite [← Nat.sub_eq_zero_iff_le]
    assumption }
  { linarith }
}
Proof state after:
no goals
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * k¡)
Tactic:
reflexivity
Proof state after:
no goals
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≤ n
Tactic:
have : k < n
Proof state after:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Theorem: binomial_symmetry_helper
Proof state before:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n

n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
{ apply lt_of_not_le
  rewrite [← Nat.sub_eq_zero_iff_le]
  assumption }
Proof state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
{ linarith }
Proof state after:
no goals
Theorem: binomial_symmetry_helper
Proof state before:
case this
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k < n
Tactic:
apply lt_of_not_le
Proof state after:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n ≤ k
Theorem: binomial_symmetry_helper
Proof state before:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n ≤ k
Tactic:
rewrite [← Nat.sub_eq_zero_iff_le]
Proof state after:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n - k = 0
Theorem: binomial_symmetry_helper
Proof state before:
case this.h
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ ¬n - k = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: binomial_symmetry_helper
Proof state before:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
this : k < n
⊢ k ≤ n
Tactic:
linarith
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
n k : ℕ
⊢ k ≤ n → (n C k) = (n C n - k)
Tactic:
intro hk_le_n
Proof state after:
n k : ℕ
hk_le_n : k ≤ n
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
n k : ℕ
hk_le_n : k ≤ n
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero n) with hn hn
Proof state after:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)

case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)

case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  sorry
}
Proof state after:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  eliminate (eq_zero_or_ne_zero k) with hk hk
  {sorry}
  {
    eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
    {
      sorry
    }
    {
      apply binomial_symmetry_helper
      {sorry}
      {sorry}
      {sorry}
    }
  }
}
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inl
n k : ℕ
hk_le_n : k ≤ n
hn : n = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero k) with hk hk
Proof state after:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)

case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)

case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{sorry}
Proof state after:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
  {
    sorry
  }
  {
    apply binomial_symmetry_helper
    {sorry}
    {sorry}
    {sorry}
  }
}
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
eliminate (eq_zero_or_ne_zero (n - k)) with hnk hnk
Proof state after:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)

case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)

case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  sorry
}
Proof state after:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
{
  apply binomial_symmetry_helper
  {sorry}
  {sorry}
  {sorry}
}
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inl
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k = 0
⊢ (n C k) = (n C n - k)
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ (n C k) = (n C n - k)
Tactic:
apply binomial_symmetry_helper
Proof state after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
Proof state after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0

case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
Proof state after:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
{sorry}
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ k ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: binomial_symmetry
Proof state before:
case inr.inr.inr.a
n k : ℕ
hk_le_n : k ≤ n
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n - k ≠ 0
Tactic:
sorry
Proof state after:
no goals
Theorem: AltChoose_zero_eq_one
Proof state before:
⊢ ∀ (n : ℕ), (n A 0) = 1
Tactic:
simp [AltChoose]
Proof state after:
no goals
Theorem: AltChoose_one_eq_self
Proof state before:
⊢ ∀ (n : ℕ), (n A 1) = n
Tactic:
sorry
Proof state after:
no goals
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
⊢ ∀ (n k : ℕ), n < k → (n A k) = 0
Tactic:
basic_induction
Proof state after:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0

case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0

case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
{
  sorry
}
Proof state after:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
{
  intro n 
  intro ih 
  sorry
}
Proof state after:
no goals
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
intro n
Proof state after:
case a
n : ℕ
⊢ (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a
n : ℕ
⊢ (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
intro ih
Proof state after:
case a
n : ℕ
ih : ∀ (k : ℕ), n < k → (n A k) = 0
⊢ ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Theorem: AltChoose_zero_of_k_gt_n
Proof state before:
case a
n : ℕ
ih : ∀ (k : ℕ), n < k → (n A k) = 0
⊢ ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: AltChoose_self_eq_one
Proof state before:
⊢ ∀ (n : ℕ), (n A n) = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: alt_binomial_symmetry
Proof state before:
⊢ ∀ (n k : ℕ), k ≤ n → (n A k) = (n A n - k)
Tactic:
sorry
Proof state after:
no goals
Theorem: BrownCs22.Nat.quotient_remainder
Proof state before:
a b c : ℕ
h : a % b = c
⊢ ∃ q, a = q * b + c
Tactic:
use a/b
Proof state after:
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c
Theorem: BrownCs22.Nat.quotient_remainder
Proof state before:
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c
Tactic:
rw [← h, mul_comm, Nat.div_add_mod]
Proof state after:
no goals
Theorem: HW4.problem_1
Proof state before:
⊢ Injective f
Tactic:
sorry
Proof state after:
no goals
Theorem: HW4.problem_2
Proof state before:
⊢ Surjective f
Tactic:
sorry
Proof state after:
no goals
Theorem: HW4.problem_3
Proof state before:
⊢ Reflexive R
Tactic:
sorry
Proof state after:
no goals
Theorem: HW4.problem_4
Proof state before:
⊢ Transitive R
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf8
Proof state before:
P : ℕ → Prop
⊢ from_three_five 8
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf9
Proof state before:
P : ℕ → Prop
⊢ from_three_five 9
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf10
Proof state before:
P : ℕ → Prop
⊢ from_three_five 10
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf_of_ge_8_le_10
Proof state before:
P : ℕ → Prop
n : ℕ
⊢ 8 ≤ n ∧ n ≤ 10 → from_three_five n
Tactic:
intro h
Proof state after:
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
⊢ from_three_five n
Theorem: ftf_of_ge_8_le_10
Proof state before:
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
⊢ from_three_five n
Tactic:
eliminate (lt_or_le n 9) with htri9 htri9
Proof state after:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
Proof state after:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
{
  eliminate (lt_or_le n 10) with htri10 htri10
  {
    sorry
  }
  {
    sorry
  }
}
Proof state after:
no goals
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals