Theorem: SimpleGraph.le_card_edgeFinset_kill (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
obtain rfl | hG := eq_or_ne G ⊥
State after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - ⊥.copyCount H ≤ (⊥.kill H).edgeFinset.card

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card

State before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
let f (H' : {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}) := (aux hG H'.2).some
State after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card

State before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
calc
  _ = H.edgeFinset.card - card {H' : H.Subgraph // Nonempty (G ≃g H'.coe)} := ?_
  _ ≤ H.edgeFinset.card - (univ.image f).card := Nat.sub_le_sub_left card_image_le _
  _ = H.edgeFinset.card - (Set.range f).toFinset.card := by rw [Set.toFinset_range]
  _ ≤ (H.edgeFinset \ (Set.range f).toFinset).card := le_card_sdiff ..
  _ = (G.kill H).edgeFinset.card := ?_
State after:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H = H.edgeFinset.card - Fintype.card { H' // Nonempty (G ≃g H'.coe) }

case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card = (G.kill H).edgeFinset.card

State before:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card = (G.kill H).edgeFinset.card
Tactic:
simp only [kill_of_ne_bot, hG, Ne, not_false_iff, Set.iUnion_singleton_eq_range,
  Set.toFinset_card, Fintype.card_ofFinset, edgeSet_deleteEdges]
State after:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card =
    Fintype.card ↑(H.edgeSet \ ⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})

State before:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card =
    Fintype.card ↑(H.edgeSet \ ⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Tactic:
simp only [Finset.sdiff_eq_inter_compl, Set.diff_eq, ← Set.iUnion_singleton_eq_range, coe_sdiff,
  Set.coe_toFinset, coe_filter, Set.sep_mem_eq, Set.iUnion_subtype, ← Fintype.card_coe,
  ← Finset.coe_sort_coe, coe_inter, coe_compl, Set.coe_toFinset, Set.compl_iUnion,
  Fintype.card_ofFinset]
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - ⊥.copyCount H ≤ (⊥.kill H).edgeFinset.card
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - (image f univ).card = H.edgeFinset.card - (Set.range f).toFinset.card
Tactic:
rw [Set.toFinset_range]
State after:
no goals

State before:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H = H.edgeFinset.card - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
Tactic:
simp only [Set.toFinset_card]
State after:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ Fintype.card ↑H.edgeSet - G.copyCount H = Fintype.card ↑H.edgeSet - Fintype.card { H' // Nonempty (G ≃g H'.coe) }

State before:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ Fintype.card ↑H.edgeSet - G.copyCount H = Fintype.card ↑H.edgeSet - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
Tactic:
rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
State after:
no goals