internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝ : k ≠ i ∧ k ≠ j
⊢ card (M.A \ MultiPart.P M k) = card (M.A \ MultiPart.P M k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝¹ : ¬(k ≠ i ∧ k ≠ j)
h✝ : k = i
⊢ card (M.A \ erase (MultiPart.P M i) v) = card (M.A \ MultiPart.P M i) + 1
Tactic:
exact card_sdiff_erase (sub_part hvi.1) hvi.2
Proof state after:
no goals
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝¹ : ¬(k ≠ i ∧ k ≠ j)
h✝ : ¬k = i
⊢ card (M.A \ insert v (MultiPart.P M j)) = card (M.A \ MultiPart.P M j) - 1
Tactic:
apply card_sdiff_insert 
  (uniq_part' hvi.1 hj.1 hj.2.symm hvi.2)
    (mem_part hvi.1 hvi.2)
Proof state after:
no goals
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a + 1) + (b + 1) * (n - b - 1)
Tactic:
rw [mul_add,add_mul,mul_one,one_mul]
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have ha := tsub_add_cancel_of_le ((le_tsub_of_add_le_left hb.le).trans tsub_le_self : 1 ≤ a)
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have h2 : a ≤ n - b := le_tsub_of_add_le_right hn
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
have hnb := tsub_add_cancel_of_le (le_trans ((le_tsub_of_add_le_left hb.le).trans tsub_le_self : 1 ≤ a) h2)
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
nth_rw 1 [← ha,← hnb]
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1 + 1) * (n - a) + b * (n - b - 1 + 1) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1 + 1) * (n - a) + b * (n - b - 1 + 1) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))
Tactic:
rw [add_mul, mul_add, one_mul, mul_one, add_assoc, add_assoc]
Proof state after:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1) * (n - a) + (n - a + (b * (n - b - 1) + b)) < (a - 1) * (n - a) + (a - 1 + (b * (n - b - 1) + (n - b - 1)))
Theorem: Turanpartition.move_change
Proof state before:
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ (a - 1) * (n - a) + (n - a + (b * (n - b - 1) + b)) < (a - 1) * (n - a) + (a - 1 + (b * (n - b - 1) + (n - b - 1)))
Tactic:
apply Nat.add_lt_add_left
Proof state after:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ n - a + (b * (n - b - 1) + b) < a - 1 + (b * (n - b - 1) + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ n - a + (b * (n - b - 1) + b) < a - 1 + (b * (n - b - 1) + (n - b - 1))
Tactic:
rw [add_comm, ← add_assoc, add_comm (a - 1), add_assoc, add_assoc]
Proof state after:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b * (n - b - 1) + (b + (n - a)) < b * (n - b - 1) + (a - 1 + (n - b - 1))
Theorem: Turanpartition.move_change
Proof state before:
case h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b * (n - b - 1) + (b + (n - a)) < b * (n - b - 1) + (a - 1 + (n - b - 1))
Tactic:
apply Nat.add_lt_add_left
Proof state after:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b + (n - a) < a - 1 + (n - b - 1)
Theorem: Turanpartition.move_change
Proof state before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
have ab : b < a - 1 := lt_tsub_of_add_lt_right hb
Proof state after:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Theorem: Turanpartition.move_change
Proof state before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
have nba : n - a < n - b - 1
Proof state after:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - b - 1

case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba : n - a < n - b - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Theorem: Turanpartition.move_change
Proof state before:
case h.h
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba : n - a < n - b - 1
⊢ b + (n - a) < a - 1 + (n - b - 1)
Tactic:
exact Nat.add_lt_add ab nba
Proof state after:
no goals
Theorem: Turanpartition.move_change
Proof state before:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - b - 1
Tactic:
have nba' : n - a < n - (b + 1)
Proof state after:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - (b + 1)

case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba' : n - a < n - (b + 1)
⊢ n - a < n - b - 1
Theorem: Turanpartition.move_change
Proof state before:
case nba
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
nba' : n - a < n - (b + 1)
⊢ n - a < n - b - 1
Tactic:
rwa [tsub_add_eq_tsub_tsub] at nba'
Proof state after:
no goals
Theorem: Turanpartition.move_change
Proof state before:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ n - a < n - (b + 1)
Tactic:
rw [tsub_lt_tsub_iff_left_of_le <| h2.trans tsub_le_self ]
Proof state after:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + 1 < a
Theorem: Turanpartition.move_change
Proof state before:
case nba'
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
ha : a - 1 + 1 = a
h2 : a ≤ n - b
hnb : n - b - 1 + 1 = n - b
ab : b < a - 1
⊢ b + 1 < a
Tactic:
exact tsub_pos_iff_lt.1 <|tsub_pos_of_lt hb
Proof state after:
no goals
Theorem: SimpleGraph.subgraph_edge_subset
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G ≤ H ↔ edgeFinset G ⊆ edgeFinset H
Tactic:
exact Iff.symm edgeFinset_subset_edgeFinset
Proof state after:
no goals
Theorem: SimpleGraph.eq_imp_edges_card_eq
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G = H → card (edgeFinset G) = card (edgeFinset H)
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : G = H
⊢ card (edgeFinset G) = card (edgeFinset H)
Theorem: SimpleGraph.eq_imp_edges_card_eq
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : G = H
⊢ card (edgeFinset G) = card (edgeFinset H)
Tactic:
rw [eq_iff_edges_eq.mp h]
Proof state after:
no goals
Theorem: SimpleGraph.empty_iff_edge_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G = ⊥ ↔ edgeFinset G = ∅
Tactic:
rw [← edgeFinset_inj,edgeFinset_bot]
Proof state after:
no goals
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G ≠ ⊥ → ∃ v w, v ≠ w ∧ Adj G v w
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ (¬∃ v w, v ≠ w ∧ Adj G v w) → ¬G ≠ ⊥
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ (¬∃ v w, v ≠ w ∧ Adj G v w) → ¬G ≠ ⊥
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬∃ v w, v ≠ w ∧ Adj G v w
⊢ ¬G ≠ ⊥
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬∃ v w, v ≠ w ∧ Adj G v w
⊢ ¬G ≠ ⊥
Tactic:
push_neg at h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ ¬G ≠ ⊥
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ ¬G ≠ ⊥
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ G = ⊥
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
⊢ G = ⊥
Tactic:
ext x x_1
Proof state after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ Adj ⊥ x x_1
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ Adj ⊥ x x_1
Tactic:
rw [bot_adj]
Proof state after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ False
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ False
Tactic:
specialize h x x_1
Proof state after:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Tactic:
by_cases h' : x = x_1
Proof state after:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : x = x_1
⊢ Adj G x x_1 ↔ False

case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : x = x_1
⊢ Adj G x x_1 ↔ False

case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Tactic:
simp only [h,h', G.irrefl]
Proof state after:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
⊢ Adj G x x_1 ↔ False
Tactic:
have := h h'
Proof state after:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
this : ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Theorem: SimpleGraph.edge_of_not_empty
Proof state before:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
x x_1 : α
h : x ≠ x_1 → ¬Adj G x x_1
h' : ¬x = x_1
this : ¬Adj G x x_1
⊢ Adj G x x_1 ↔ False
Tactic:
tauto
Proof state after:
no goals
Theorem: SimpleGraph.two_cliqueFree_imp_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ CliqueFree G 2 → G = ⊥
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : CliqueFree G 2
⊢ G = ⊥
Theorem: SimpleGraph.two_cliqueFree_imp_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : CliqueFree G 2
⊢ G = ⊥
Tactic:
contrapose h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
⊢ ¬CliqueFree G 2
Theorem: SimpleGraph.two_cliqueFree_imp_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
⊢ ¬CliqueFree G 2
Tactic:
obtain ⟨v, w, had⟩ := edge_of_not_empty h
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
⊢ ¬CliqueFree G 2
Theorem: SimpleGraph.two_cliqueFree_imp_empty
Proof state before:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
⊢ ¬CliqueFree G 2
Tactic:
intro hf
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
hf : CliqueFree G 2
⊢ False
Theorem: SimpleGraph.two_cliqueFree_imp_empty
Proof state before:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ¬G = ⊥
v w : α
had : v ≠ w ∧ Adj G v w
hf : CliqueFree G 2
⊢ False
Tactic:
apply hf _ (adj_is2Clique had.2)
Proof state after:
no goals
Theorem: SimpleGraph.disjoint_edges_iff_meet_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ Disjoint (edgeFinset G) (edgeFinset H) ↔ G ⊓ H = ⊥
Tactic:
rw [disjoint_iff,← edgeFinset_inj,edgeFinset_inf,inf_eq_inter,edgeFinset_bot,bot_eq_empty]
Proof state after:
no goals
Theorem: SimpleGraph.card_edges_add_of_meet_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G ⊓ H = ⊥ → card (edgeFinset (G ⊔ H)) = card (edgeFinset G) + card (edgeFinset H)
Tactic:
rw [← disjoint_edges_iff_meet_empty,edgeFinset_sup]
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ Disjoint (edgeFinset G) (edgeFinset H) →
    card (edgeFinset G ∪ edgeFinset H) = card (edgeFinset G) + card (edgeFinset H)
Theorem: SimpleGraph.card_edges_add_of_meet_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ Disjoint (edgeFinset G) (edgeFinset H) →
    card (edgeFinset G ∪ edgeFinset H) = card (edgeFinset G) + card (edgeFinset H)
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : Disjoint (edgeFinset G) (edgeFinset H)
⊢ card (edgeFinset G ∪ edgeFinset H) = card (edgeFinset G) + card (edgeFinset H)
Theorem: SimpleGraph.card_edges_add_of_meet_empty
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : Disjoint (edgeFinset G) (edgeFinset H)
⊢ card (edgeFinset G ∪ edgeFinset H) = card (edgeFinset G) + card (edgeFinset H)
Tactic:
exact card_disjoint_union h
Proof state after:
no goals
Theorem: SimpleGraph.delFedges_is_sdiff
Proof state before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
⊢ delFedges G (edgeFinset H) = G \ H
Tactic:
ext u v
Proof state after:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj (delFedges G (edgeFinset H)) u v ↔ Adj (G \ H) u v
Theorem: SimpleGraph.delFedges_is_sdiff
Proof state before:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj (delFedges G (edgeFinset H)) u v ↔ Adj (G \ H) u v
Tactic:
simp only [delFedges, sdiff_adj, Set.coe_toFinset,  Sym2.toRel_prop, mem_edgeSet]
Proof state after:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj G u v \ Adj H u v ↔ Adj G u v ∧ ¬Adj H u v
Theorem: SimpleGraph.delFedges_is_sdiff
Proof state before:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj G u v \ Adj H u v ↔ Adj G u v ∧ ¬Adj H u v
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.isFar_le
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
⊢ IsFar G H s → IsFar G H t
Tactic:
intro h1
Proof state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
h1 : IsFar G H s
⊢ IsFar G H t
Theorem: SimpleGraph.isFar_le
Proof state before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
h1 : IsFar G H s
⊢ IsFar G H t
Tactic:
obtain ⟨S, hS1, hS2⟩ := h1
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
S : Finset (Sym2 α)
hS1 : delFedges G S ≤ H
hS2 : card S ≤ s
⊢ IsFar G H t