internlm/Lean-Github huggingface dataset:
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ n - r - (n - 2 * r) = r
Tactic:
rw [tsub_right_comm, Nat.sub_sub_self, two_mul]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ r + r - r = r

α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ 2 * r ≤ n
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ r + r - r = r

α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ 2 * r ≤ n
Tactic:
apply Nat.add_sub_cancel
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ 2 * r ≤ n
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ 2 * r ≤ n
Tactic:
rw [mul_comm, ← Nat.le_div_iff_mul_le' zero_lt_two]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ r ≤ n / 2
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ r ≤ n / 2
Tactic:
exact h₃
Proof state after:
no goals
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n.choose r < (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card
Tactic:
rw [card_union_of_disjoint ‹_›]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n.choose r < 𝒜.card + (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
Theorem: Finset.EKR
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n.choose r < 𝒜.card + (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
Tactic:
convert lt_of_le_of_lt (add_le_add_left kk _) (add_lt_add_right size _) using 1
Proof state after:
case h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r
Theorem: Finset.EKR
Proof state before:
case h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r
Tactic:
convert Nat.choose_succ_succ _ _ using 3
Proof state after:
case h.e'_2.h.e'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n = (n - 1).succ

case h.e'_2.h.e'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ

case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ
Theorem: Finset.EKR
Proof state before:
case h.e'_2.h.e'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ n = (n - 1).succ

case h.e'_2.h.e'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ

case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ
Tactic:
all_goals rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
Proof state after:
no goals
Theorem: Finset.EKR
Proof state before:
case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝² : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
⊢ r = (r - 1).succ
Tactic:
rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
Proof state after:
no goals
Theorem: Finset.EKR
Proof state before:
case h.e'_4.h.e'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < 𝒜.card
this✝³ : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ)
this✝² : r ≤ n
this✝¹ : 1 ≤ n
z : (n - 1).choose (n - r) < 𝒜ᶜˢ.card
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
this✝ : n - 2 * r ≤ n - r
kk : (n - 1).choose r ≤ (∂ ^[n - 2 * r] 𝒜ᶜˢ).card
q : n - r - (n - 2 * r) = r
this : n.choose r < (𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ).card
⊢ n = Fintype.card (Fin n)
Tactic:
rw [Fintype.card_fin]
Proof state after:
no goals
Theorem: List.finite_length_eq
Proof state before:
case zero
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length = 0}.Finite
Tactic:
simp [List.length_eq_zero]
Proof state after:
no goals
Theorem: List.finite_length_eq
Proof state before:
case succ
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
⊢ {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
Tactic:
ext (_ | _) <;> simp [n.succ_ne_zero.symm]
Proof state after:
no goals
Theorem: List.finite_length_eq
Proof state before:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ {l | l.length = n + 1}.Finite
Tactic:
rw [this]
Proof state after:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ (image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}).Finite
Theorem: List.finite_length_eq
Proof state before:
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ (image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}).Finite
Tactic:
exact Set.finite_univ.image2 _ ih
Proof state after:
no goals
Theorem: List.finite_length_lt
Proof state before:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite
Tactic:
convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i
Proof state after:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Theorem: List.finite_length_lt
Proof state before:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Tactic:
ext
Proof state after:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Theorem: List.finite_length_lt
Proof state before:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Tactic:
simp
Proof state after:
no goals
Theorem: List.finite_length_le
Proof state before:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length ≤ n}.Finite
Tactic:
simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)
Proof state after:
no goals
Theorem: Multiset.exists_intermediate
Proof state before:
α : Type u_1
s t : Multiset α
n : ℕ
hst : s ≤ t
hs : card s ≤ n
ht : n ≤ card t
⊢ ∃ u, s ≤ u ∧ u ≤ t ∧ card u = n
Tactic:
induction' s using Quotient.inductionOn with l₀
Proof state after:
case h
α : Type u_1
s t : Multiset α
n : ℕ
ht : n ≤ card t
l₀ : List α
hst : ⟦l₀⟧ ≤ t
hs : card ⟦l₀⟧ ≤ n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ t ∧ card u = n
Theorem: Multiset.exists_intermediate
Proof state before:
case h
α : Type u_1
s t : Multiset α
n : ℕ
ht : n ≤ card t
l₀ : List α
hst : ⟦l₀⟧ ≤ t
hs : card ⟦l₀⟧ ≤ n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ t ∧ card u = n
Tactic:
induction' t using Quotient.inductionOn with l₂
Proof state after:
case h.h
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Theorem: Multiset.exists_intermediate
Proof state before:
case h.h
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Tactic:
obtain ⟨l₁, h⟩ := hst.exists_intermediate hs ht
Proof state after:
case h.h.intro
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
l₁ : List α
h : l₀.Subperm l₁ ∧ l₁.Subperm l₂ ∧ l₁.length = n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Theorem: Multiset.exists_intermediate
Proof state before:
case h.h.intro
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
l₁ : List α
h : l₀.Subperm l₁ ∧ l₁.Subperm l₂ ∧ l₁.length = n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Tactic:
exact ⟨l₁, h⟩
Proof state after:
no goals
Theorem: Multiset.exists_le_card_eq
Proof state before:
α : Type u_1
s t : Multiset α
n : ℕ
hn : n ≤ card s
⊢ ∃ t ≤ s, card t = n
Tactic:
simpa using exists_intermediate (zero_le _) (Nat.zero_le _) hn
Proof state after:
no goals
Theorem: Finset.sum_boole_mul'
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : ι
⊢ ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0
Tactic:
simp
Proof state after:
no goals
Theorem: GraphTheory.ES1.q4
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected
Tactic:
cases nonempty_fintype α
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
val✝ : Fintype α
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected
Theorem: GraphTheory.ES1.q4
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
val✝ : Fintype α
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected
Tactic:
sorry
Proof state after:
no goals
Theorem: GraphTheory.ES1.q5
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
cases isEmpty_or_nonempty α
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : IsEmpty α
⊢ G.edgeFinset.card ≤ card α - 1

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : Nonempty α
⊢ G.edgeFinset.card ≤ card α - 1
Theorem: GraphTheory.ES1.q5
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : Nonempty α
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
sorry
Proof state after:
no goals
Theorem: GraphTheory.ES1.q5
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : IsEmpty α
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
simp
Proof state after:
no goals
Theorem: List.length_rtake
Proof state before:
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m n✝ n : ℕ
l : List α
⊢ l.length - (l.length - n) = min n l.length
Tactic:
rw [Nat.sub_sub_eq_min, min_comm]
Proof state after:
no goals
Theorem: List.take_reverse
Proof state before:
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m n✝ n : ℕ
l : List α
⊢ take n l.reverse = (l.rtake n).reverse
Tactic:
rw [rtake_eq_reverse_take_reverse, reverse_reverse]
Proof state after:
no goals
Theorem: List.rtake_reverse
Proof state before:
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m n✝ n : ℕ
l : List α
⊢ l.reverse.rtake n = (take n l).reverse
Tactic:
rw [rtake_eq_reverse_take_reverse, reverse_reverse]
Proof state after:
no goals
Theorem: List.rtake_rtake
Proof state before:
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m✝ n✝ n m : ℕ
l : List α
⊢ (l.rtake m).rtake n = l.rtake (min n m)
Tactic:
rw [rtake_eq_reverse_take_reverse, ← take_reverse, take_take, rtake_eq_reverse_take_reverse]
Proof state after:
no goals
Theorem: List.take_prefix_take
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : m ≤ n
⊢ take m l <+: take n l
Tactic:
rw [prefix_iff_eq_take, length_take, take_take, min_right_comm, min_eq_left h, take_min]
Proof state after:
no goals
Theorem: List.IsPrefix.take
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ l <+: take n l'
Tactic:
rw [hl.eq_take]
Proof state after:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ take l.length l' <+: take n l'
Theorem: List.IsPrefix.take
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ take l.length l' <+: take n l'
Tactic:
exact take_prefix_take h
Proof state after:
no goals
Theorem: List.IsSuffix.rtake
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l <:+ l'.rtake n
Tactic:
rw [hl.eq_rtake]
Proof state after:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l'.rtake l.length <:+ l'.rtake n
Theorem: List.IsSuffix.rtake
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l'.rtake l.length <:+ l'.rtake n
Tactic:
exact rtake_suffix_rtake h
Proof state after:
no goals
Theorem: List.Sublist.exists_intermediate
Proof state before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
induction' l₀ with a l₀ ih generalizing n l₂
Proof state after:
case nil
α : Type u_1
l l' l₁ : List α
a b : α
m : ℕ
l₂ : List α
n : ℕ
hl : [] <+ l₂
h₀ : [].length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, [] <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n

case cons
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
n : ℕ
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
n : ℕ
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
Tactic:
cases n
Proof state after:
case cons.zero
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ 0
h₂ : 0 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = 0

case cons.succ
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
h₂ : n✝ + 1 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n✝ + 1
Theorem: List.Sublist.exists_intermediate
Proof state before:
case cons.succ
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
hl : a :: l₀ <+ l₂
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
h₂ : n✝ + 1 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n✝ + 1
Tactic:
cases' l₂ with b l₂
Proof state after:
case cons.succ.nil
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
hl : a :: l₀ <+ []
h₂ : n✝ + 1 ≤ [].length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ [] ∧ l₁.length = n✝ + 1

case cons.succ.cons
α : Type u_1
l l' l₁ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1