internlm/Lean-Github huggingface dataset:
Theorem: exp_factorial_bound
Proof state before:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ rexp x
Tactic:
rw [exp_eq_exp_ℝ]
Proof state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ _root_.exp ℝ x
Theorem: exp_factorial_bound
Proof state before:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ x ^ n / ↑n ! ≤ _root_.exp ℝ x
Tactic:
exact le_hasSum (expSeries_div_hasSum_exp ℝ x) n (fun _ _ => by positivity)
Proof state after:
no goals
Theorem: exp_factorial_bound
Proof state before:
x : ℝ
hx : 0 ≤ x
n x✝¹ : ℕ
x✝ : x✝¹ ≠ n
⊢ 0 ≤ x ^ x✝¹ / ↑x✝¹!
Tactic:
positivity
Proof state after:
no goals
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < rexp x
Tactic:
rw [exp_eq_exp_ℝ]
Proof state after:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < _root_.exp ℝ x
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < _root_.exp ℝ x
Tactic:
refine (sum_le_hasSum {n, 0} ?_ (expSeries_div_hasSum_exp ℝ x)).trans_lt' ?_
Proof state after:
case refine_1
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ ∀ i ∉ {n, 0}, 0 ≤ x ^ i / ↑i !

case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < Finset.sum {n, 0} fun i => x ^ i / ↑i !
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < Finset.sum {n, 0} fun i => x ^ i / ↑i !
Tactic:
rw [sum_pair hn]
Proof state after:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < x ^ n / ↑n ! + x ^ 0 / ↑0!
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < x ^ n / ↑n ! + x ^ 0 / ↑0!
Tactic:
simp
Proof state after:
no goals
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
case refine_1
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ ∀ i ∉ {n, 0}, 0 ≤ x ^ i / ↑i !
Tactic:
intro x _
Proof state after:
case refine_1
n : ℕ
x✝ : ℝ
hx : 0 ≤ x✝
hn : n ≠ 0
x : ℕ
a✝ : x ∉ {n, 0}
⊢ 0 ≤ x✝ ^ x / ↑x !
Theorem: exp_factorial_bound_of_ne_zero
Proof state before:
case refine_1
n : ℕ
x✝ : ℝ
hx : 0 ≤ x✝
hn : n ≠ 0
x : ℕ
a✝ : x ∉ {n, 0}
⊢ 0 ≤ x✝ ^ x / ↑x !
Tactic:
positivity
Proof state after:
no goals
Theorem: factorial_bound_exp
Proof state before:
n : ℕ
⊢ (↑n / rexp 1) ^ n ≤ ↑n !
Tactic:
rw [div_pow, ← rpow_nat_cast (exp 1), exp_one_rpow, div_le_iff, ← div_le_iff']
Proof state after:
n : ℕ
⊢ ↑n ^ n / ↑n ! ≤ rexp ↑n

n : ℕ
⊢ 0 < ↑n !

n : ℕ
⊢ 0 < rexp ↑n
Theorem: factorial_bound_exp
Proof state before:
n : ℕ
⊢ ↑n ^ n / ↑n ! ≤ rexp ↑n
Tactic:
exact exp_factorial_bound (Nat.cast_nonneg _)
Proof state after:
no goals
Theorem: factorial_bound_exp
Proof state before:
n : ℕ
⊢ 0 < ↑n !
Tactic:
positivity
Proof state after:
no goals
Theorem: factorial_bound_exp
Proof state before:
n : ℕ
⊢ 0 < rexp ↑n
Tactic:
positivity
Proof state after:
no goals
Theorem: factorial_bound_exp_of_ne_zero
Proof state before:
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n < ↑n !
Tactic:
rw [div_pow, ← rpow_nat_cast (exp 1), exp_one_rpow, div_lt_iff, ← div_lt_iff']
Proof state after:
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ n / ↑n ! < rexp ↑n

n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n !

n : ℕ
hn : n ≠ 0
⊢ 0 < rexp ↑n
Theorem: factorial_bound_exp_of_ne_zero
Proof state before:
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ n / ↑n ! < rexp ↑n
Tactic:
exact exp_factorial_bound_of_ne_zero (Nat.cast_nonneg _) hn
Proof state after:
no goals
Theorem: factorial_bound_exp_of_ne_zero
Proof state before:
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n !
Tactic:
positivity
Proof state after:
no goals
Theorem: factorial_bound_exp_of_ne_zero
Proof state before:
n : ℕ
hn : n ≠ 0
⊢ 0 < rexp ↑n
Tactic:
positivity
Proof state after:
no goals
Theorem: Nat.choose_le_pow'
Proof state before:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(choose n r) ≤ ↑n ^ r / ↑r !
Tactic:
simpa using Nat.choose_le_pow (α := α) r n
Proof state after:
no goals
Theorem: choose_upper_bound
Proof state before:
n t : ℕ
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
cases' Nat.eq_zero_or_pos t with h h
Proof state after:
case inl
n t : ℕ
h : t = 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t

case inr
n t : ℕ
h : t > 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Theorem: choose_upper_bound
Proof state before:
case inr
n t : ℕ
h : t > 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (Nat.choose_le_pow' t n).trans _
Proof state after:
case inr
n t : ℕ
h : t > 0
⊢ ↑n ^ t / ↑t ! ≤ (rexp 1 * ↑n / ↑t) ^ t
Theorem: choose_upper_bound
Proof state before:
case inr
n t : ℕ
h : t > 0
⊢ ↑n ^ t / ↑t ! ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (div_le_div_of_le_left _ _ factorial_bound_exp).trans _
Proof state after:
case inr.refine'_1
n t : ℕ
h : t > 0
⊢ 0 ≤ ↑n ^ t

case inr.refine'_2
n t : ℕ
h : t > 0
⊢ 0 < (↑t / rexp 1) ^ t

case inr.refine'_3
n t : ℕ
h : t > 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t ≤ (rexp 1 * ↑n / ↑t) ^ t
Theorem: choose_upper_bound
Proof state before:
case inr.refine'_3
n t : ℕ
h : t > 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
rw [← div_pow, div_div_eq_mul_div, mul_comm]
Proof state after:
no goals
Theorem: choose_upper_bound
Proof state before:
case inl
n t : ℕ
h : t = 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
Tactic:
simp [h]
Proof state after:
no goals
Theorem: choose_upper_bound
Proof state before:
case inr.refine'_1
n t : ℕ
h : t > 0
⊢ 0 ≤ ↑n ^ t
Tactic:
positivity
Proof state after:
no goals
Theorem: choose_upper_bound
Proof state before:
case inr.refine'_2
n t : ℕ
h : t > 0
⊢ 0 < (↑t / rexp 1) ^ t
Tactic:
positivity
Proof state after:
no goals
Theorem: choose_upper_bound_of_pos
Proof state before:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑(Nat.choose n t) < (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (Nat.choose_le_pow' t n).trans_lt _
Proof state after:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / ↑t ! < (rexp 1 * ↑n / ↑t) ^ t
Theorem: choose_upper_bound_of_pos
Proof state before:
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / ↑t ! < (rexp 1 * ↑n / ↑t) ^ t
Tactic:
refine' (div_lt_div_of_lt_left _ _ (factorial_bound_exp_of_ne_zero ht)).trans_eq _
Proof state after:
case refine'_1
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < ↑n ^ t

case refine'_2
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < (↑t / rexp 1) ^ t

case refine'_3
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t = (rexp 1 * ↑n / ↑t) ^ t
Theorem: choose_upper_bound_of_pos
Proof state before:
case refine'_3
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t = (rexp 1 * ↑n / ↑t) ^ t
Tactic:
rw [← div_pow, div_div_eq_mul_div, mul_comm]
Proof state after:
no goals
Theorem: choose_upper_bound_of_pos
Proof state before:
case refine'_1
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < ↑n ^ t
Tactic:
positivity
Proof state after:
no goals
Theorem: choose_upper_bound_of_pos
Proof state before:
case refine'_2
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < (↑t / rexp 1) ^ t
Tactic:
positivity
Proof state after:
no goals
Theorem: choose_upper_bound'
Proof state before:
n t : ℕ
⊢ (rexp 1 * ↑n / ↑t) ^ t = rexp ↑t * (↑n / ↑t) ^ t
Tactic:
rw [mul_div_assoc, mul_pow, ← exp_one_rpow t, rpow_nat_cast]
Proof state after:
no goals
Theorem: SimpleGraph.card_top_edgeSet
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Fintype.card ↑(edgeSet ⊤) = Nat.choose (Fintype.card V) 2
Tactic:
rw [Fintype.card_congr topEdgeSetEquiv, Sym2.card_subtype_not_diag]
Proof state after:
no goals
Theorem: SimpleGraph.edgeSet_eq_empty_iff
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G : SimpleGraph V
⊢ edgeSet G = ∅ ↔ G = ⊥
Tactic:
rw [← edgeSet_bot, edgeSet_inj]
Proof state after:
no goals
Theorem: SimpleGraph.disjoint_edgeSet
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
⊢ Disjoint (edgeSet G) (edgeSet H) ↔ Disjoint G H
Tactic:
rw [Set.disjoint_iff_inter_eq_empty, disjoint_iff, ← edgeSet_inf, edgeSet_eq_empty_iff]
Proof state after:
no goals
Theorem: SimpleGraph.disjoint_left
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
⊢ Disjoint G H ↔ ∀ (x y : V), Adj G x y → ¬Adj H x y
Tactic:
simp only [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall, mem_edgeSet]
Proof state after:
no goals
Theorem: SimpleGraph.adj_sup_iff
Proof state before:
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
s : Finset ι
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
Tactic:
induction' s using Finset.cons_induction_on with a s has ih
Proof state after:
case h₁
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup ∅ f) x y ↔ ∃ i ∈ ∅, Adj (f i) x y

case h₂
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
a : ι
s : Finset ι
has : a ∉ s
ih : Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
⊢ Adj (sup (cons a s has) f) x y ↔ ∃ i ∈ cons a s has, Adj (f i) x y
Theorem: SimpleGraph.adj_sup_iff
Proof state before:
case h₁
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
⊢ Adj (sup ∅ f) x y ↔ ∃ i ∈ ∅, Adj (f i) x y
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.adj_sup_iff
Proof state before:
case h₂
V✝ : Type u_1
V' : Type u_2
G : SimpleGraph V✝
K : Type u_3
K' : Type u_4
ι : Type u_5
V : Type u_6
f : ι → SimpleGraph V
x y : V
a : ι
s : Finset ι
has : a ∉ s
ih : Adj (sup s f) x y ↔ ∃ i ∈ s, Adj (f i) x y
⊢ Adj (sup (cons a s has) f) x y ↔ ∃ i ∈ cons a s has, Adj (f i) x y
Tactic:
simp [or_and_right, exists_or, ih]
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_bot
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x : V
⊢ neighborSet ⊥ x = ∅
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborSet ⊥ x ↔ y ∈ ∅
Theorem: SimpleGraph.neighborSet_bot
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborSet ⊥ x ↔ y ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_top
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x : V
⊢ neighborSet ⊤ x = {x}ᶜ
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborSet ⊤ x ↔ y ∈ {x}ᶜ
Theorem: SimpleGraph.neighborSet_top
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborSet ⊤ x ↔ y ∈ {x}ᶜ
Tactic:
rw [mem_neighborSet, top_adj, Set.mem_compl_singleton_iff, ne_comm]
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_sup
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
⊢ neighborSet (G ⊔ H) x = neighborSet G x ∪ neighborSet H x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊔ H) x ↔ y ∈ neighborSet G x ∪ neighborSet H x
Theorem: SimpleGraph.neighborSet_sup
Proof state before:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊔ H) x ↔ y ∈ neighborSet G x ∪ neighborSet H x
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_inf
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
⊢ neighborSet (G ⊓ H) x = neighborSet G x ∩ neighborSet H x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊓ H) x ↔ y ∈ neighborSet G x ∩ neighborSet H x
Theorem: SimpleGraph.neighborSet_inf
Proof state before:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊓ H) x ↔ y ∈ neighborSet G x ∩ neighborSet H x
Tactic:
simp only [mem_neighborSet, inf_adj, Set.mem_inter_iff]
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_iSup
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x : V
⊢ neighborSet (⨆ i, s i) x = ⋃ i, neighborSet (s i) x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨆ i, s i) x ↔ y ∈ ⋃ i, neighborSet (s i) x
Theorem: SimpleGraph.neighborSet_iSup
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨆ i, s i) x ↔ y ∈ ⋃ i, neighborSet (s i) x
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_iInf
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x : V
⊢ neighborSet (⨅ i, s i) x = ⋂ i, neighborSet (s i) x
Tactic:
ext y
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨅ i, s i) x ↔ y ∈ ⋂ i, neighborSet (s i) x
Theorem: SimpleGraph.neighborSet_iInf
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ y ∈ neighborSet (⨅ i, s i) x ↔ y ∈ ⋂ i, neighborSet (s i) x
Tactic:
simp only [mem_neighborSet, iInf_adj, Ne.def, Set.iInf_eq_iInter, Set.mem_iInter,
  and_iff_left_iff_imp]
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ (∀ (i : ι), Adj (s i) x y) → ¬x = y
Theorem: SimpleGraph.neighborSet_iInf
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
⊢ (∀ (i : ι), Adj (s i) x y) → ¬x = y
Tactic:
intro h
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
⊢ ¬x = y
Theorem: SimpleGraph.neighborSet_iInf
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
⊢ ¬x = y
Tactic:
inhabit ι
Proof state after:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
inhabited_h : Inhabited ι
⊢ ¬x = y
Theorem: SimpleGraph.neighborSet_iInf
Proof state before:
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
ι : Type u_5
inst✝ : Nonempty ι
s : ι → SimpleGraph V
x y : V
h : ∀ (i : ι), Adj (s i) x y
inhabited_h : Inhabited ι
⊢ ¬x = y
Tactic:
exact (h default).ne
Proof state after:
no goals
Theorem: SimpleGraph.neighborSet_disjoint
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)
Tactic:
rw [Set.disjoint_iff_inter_eq_empty, ← neighborSet_inf, h.eq_bot, neighborSet_bot]
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_bot
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x : V
⊢ neighborFinset ⊥ x = ∅
Tactic:
ext y
Proof state after:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborFinset ⊥ x ↔ y ∈ ∅
Theorem: SimpleGraph.neighborFinset_bot
Proof state before:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborFinset ⊥ x ↔ y ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_top
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x : V
⊢ neighborFinset ⊤ x = {x}ᶜ
Tactic:
ext y
Proof state after:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x y : V
⊢ y ∈ neighborFinset ⊤ x ↔ y ∈ {x}ᶜ
Theorem: SimpleGraph.neighborFinset_top
Proof state before:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : Fintype V
inst✝ : DecidableEq V
x y : V
⊢ y ∈ neighborFinset ⊤ x ↔ y ∈ {x}ᶜ
Tactic:
rw [mem_neighborFinset, top_adj, Finset.mem_compl, mem_singleton, ne_comm]
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_sup
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊔ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
⊢ neighborFinset (G ⊔ H) x = neighborFinset G x ∪ neighborFinset H x
Tactic:
ext y
Proof state after:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊔ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊔ H) x ↔ y ∈ neighborFinset G x ∪ neighborFinset H x
Theorem: SimpleGraph.neighborFinset_sup
Proof state before:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊔ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊔ H) x ↔ y ∈ neighborFinset G x ∪ neighborFinset H x
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_inf
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
⊢ neighborFinset (G ⊓ H) x = neighborFinset G x ∩ neighborFinset H x
Tactic:
ext y
Proof state after:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊓ H) x ↔ y ∈ neighborFinset G x ∩ neighborFinset H x
Theorem: SimpleGraph.neighborFinset_inf
Proof state before:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊓ H) x ↔ y ∈ neighborFinset G x ∩ neighborFinset H x
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_supr
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
⊢ neighborFinset (sup s f) x = Finset.biUnion s fun i => neighborFinset (f i) x
Tactic:
ext y
Proof state after:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
y : V
⊢ y ∈ neighborFinset (sup s f) x ↔ y ∈ Finset.biUnion s fun i => neighborFinset (f i) x
Theorem: SimpleGraph.neighborFinset_supr
Proof state before:
case a
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝² : DecidableEq V
ι : Type u_5
s : Finset ι
f : ι → SimpleGraph V
x : V
inst✝¹ : (i : ι) → Fintype ↑(neighborSet (f i) x)
inst✝ : Fintype ↑(neighborSet (sup s f) x)
y : V
⊢ y ∈ neighborFinset (sup s f) x ↔ y ∈ Finset.biUnion s fun i => neighborFinset (f i) x
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.coe_neighborFinset
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G : SimpleGraph V
x : V
inst✝ : Fintype ↑(neighborSet G x)
⊢ ↑(neighborFinset G x) = neighborSet G x
Tactic:
rw [neighborFinset_def, Set.coe_toFinset]
Proof state after:
no goals
Theorem: SimpleGraph.neighborFinset_disjoint
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborFinset G x) (neighborFinset H x)
Tactic:
rw [← disjoint_coe, coe_neighborFinset, coe_neighborFinset]
Proof state after:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)
Theorem: SimpleGraph.neighborFinset_disjoint
Proof state before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x : V
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)
Tactic:
exact neighborSet_disjoint h
Proof state after:
no goals
Theorem: SimpleGraph.degree_eq_zero_iff
Proof state before:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
v : V
inst✝ : Fintype ↑(neighborSet G v)
⊢ degree G v = 0 ↔ ∀ (w : V), ¬Adj G v w
Tactic:
rw [← not_exists, ← degree_pos_iff_exists_adj, not_lt, le_zero_iff]
Proof state after:
no goals
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : filter (fun x => Odd (degree G x)) univ ≠ univ
⊢ ∃ v, Even (degree G v)
Tactic:
rw [Ne.def, filter_eq_self] at this
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : ¬∀ x ∈ univ, Odd (degree G x)
⊢ ∃ v, Even (degree G v)
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : ¬∀ x ∈ univ, Odd (degree G x)
⊢ ∃ v, Even (degree G v)
Tactic:
simpa using this
Proof state after:
no goals
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ filter (fun x => Odd (degree G x)) univ ≠ univ
Tactic:
rw [←card_lt_iff_ne_univ, (card_le_univ _).lt_iff_ne]
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ Finset.card (filter (fun x => Odd (degree G x)) univ) ≠ Fintype.card V
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ Finset.card (filter (fun x => Odd (degree G x)) univ) ≠ Fintype.card V
Tactic:
intro h
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
⊢ False
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
⊢ False
Tactic:
have h' := even_card_odd_degree_vertices G
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : Even (Finset.card (filter (fun v => Odd (degree G v)) univ))
⊢ False