awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
rw rw₁ rw₂ : Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)} = 1
h :
  Eq (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)}
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}
h₁ :
  Nonempty.{u_1 + 1}
      (Iso (V := V) (W := (↑Set.univ : Type u_1)) ⊥
        (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } :
          SimpleGraph
            (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) :
              Type u_1))) ∧
    ∀ (x : G.Subgraph) (a : Iso (V := V) ⊥ x.coe),
      x = { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
h₂ :
  ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe),
    H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
h₃ :
  ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe) (a b : V),
    H'.Adj a b ↔ Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ } a b
h₄ : ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe) (a b : V), ¬H'.Adj a b
⊢ G.copyCount (W := V) ⊥ = 1

Tactic:
classical
  rw [copyCount]
  convert!
    card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }
  simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]
  refine ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
    Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩
  ext a b
  simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false]
  exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe

Premises used: SimpleGraph.Subgraph.mk, iff_false, Nonempty.forall, Set.univ, False.elim, Finset.mem_filter_univ, Prop.bot_eq_false, Pi.bot_apply, Bot.bot, Finset.eq_singleton_iff_unique_mem, SimpleGraph.copyCount, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
intro : ∀ (val : Fintype W), G.copyCount H = 1
⊢ G.copyCount H = 1

Tactic:
cases nonempty_fintype W

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
val : Fintype W
⊢ G.copyCount H = 1

Tactic:
(copyCount_le_labelledCopyCount.trans_eq <| labelledCopyCount_of_isEmpty ..).antisymm <|
    copyCount_pos.2 <| .of_isEmpty

Premises used: Iff.mpr, LE.le.trans_eq, LE.le.antisymm, SimpleGraph.IsContained.of_isEmpty, SimpleGraph.copyCount_pos, SimpleGraph.copyCount_le_labelledCopyCount, SimpleGraph.labelledCopyCount_of_isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
val : Fintype W
⊢ G.copyCount H = 1

Tactic:
exact (copyCount_le_labelledCopyCount.trans_eq <| labelledCopyCount_of_isEmpty ..).antisymm <|
    copyCount_pos.2 <| .of_isEmpty

Premises used: Iff.mpr, LE.le.trans_eq, LE.le.antisymm, SimpleGraph.copyCount_pos, SimpleGraph.copyCount_le_labelledCopyCount, SimpleGraph.labelledCopyCount_of_isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
obtain : ∀ (e : Sym2 W) (he : e ∈ H.edgeSet), Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty
⊢ Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty

Tactic:
obtain ⟨e, he⟩ := edgeSet_nonempty.2 hH

Premises used: Iff.mpr, SimpleGraph.edgeSet_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
rw : Nonempty (H ≃g G'.coe) → (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet).Nonempty
⊢ Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty

Tactic:
rw [← Subgraph.image_coe_edgeSet_coe]

Premises used: SimpleGraph.Subgraph.image_coe_edgeSet_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet).Nonempty

Tactic:
fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩

Premises used: Iff.mpr, Sym2.map, SimpleGraph.Iso.map_mem_edgeSet_iff, SimpleGraph.edgeSet, Set.Nonempty, SimpleGraph.Subgraph.coe, Set.Nonempty.image, Exists.intro, Set.image, Subtype.val, DFunLike.coe, _private.0.SimpleGraph.aux.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet).Nonempty

Tactic:
exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
G : SimpleGraph V
H : SimpleGraph W
⊢ SimpleGraph V

Tactic:
exact
  if hH : H = ⊥ then G
  else G.deleteEdges <| ⋃ (G' : G.Subgraph) (hG' : Nonempty (H ≃g G'.coe)), {(aux hH hG').some}

Premises used: SimpleGraph.deleteEdges, SimpleGraph.Subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G_1 G₁ G₂ G₃ : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
G : SimpleGraph V
H : SimpleGraph W
⊢ SimpleGraph V

Tactic:
classical exact
  if hH : H = ⊥ then G
  else G.deleteEdges <| ⋃ (G' : G.Subgraph) (hG' : Nonempty (H ≃g G'.coe)), {(aux hH hG').some}

Premises used: SimpleGraph.deleteEdges, SimpleGraph.Subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
simp : sorry = G ↔ ∀ (x : G.Subgraph), IsEmpty (H ≃g x.coe)
⊢ sorry = G ↔ H.Free G

Tactic:
simp only [killCopies_of_ne_bot hH, Set.disjoint_left, isContained_iff_exists_iso_subgraph,
    @forall_comm _ G.Subgraph, deleteEdges_eq_self, Set.mem_iUnion,
    not_exists, not_nonempty_iff, Nonempty.forall, Free]

Premises used: SimpleGraph.Free, SimpleGraph.isContained_iff_exists_iso_subgraph, Nonempty.forall, Set.disjoint_left, Set.mem_iUnion, forall_comm, not_exists, _private.0.SimpleGraph.killCopies_of_ne_bot, not_nonempty_iff, SimpleGraph.deleteEdges_eq_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ sorry = G ↔ ∀ (x : G.Subgraph), IsEmpty (H ≃g x.coe)

Tactic:
forall_congr' fun G' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
    (Subgraph.edgeSet_subset _ <| (aux hH ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
inl : ∀ (hHG : Free.{u_2, u_1} (α := W) ⊥ G), sorry = G
inr : ∀ (hH : H ≠ ⊥), sorry = G
⊢ sorry = G

Tactic:
obtain rfl | hH := eq_or_ne H ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : Free.{u_2, u_1} (α := W) ⊥ G
⊢ sorry = G

Tactic:
killCopies_bot _

Premises used: SimpleGraph.killCopies_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : Free.{u_2, u_1} (α := W) ⊥ G
⊢ sorry = G

Tactic:
exact killCopies_bot _

Premises used: SimpleGraph.killCopies_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ sorry = G

Tactic:
(killCopies_eq_left hH).2 hHG

Premises used: Iff.mpr, SimpleGraph.killCopies_eq_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ sorry = G

Tactic:
exact (killCopies_eq_left hH).2 hHG

Premises used: Iff.mpr, SimpleGraph.killCopies_eq_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
inl :
  #G.edgeFinset - copyCount.{u_1, u_2} (W := W) G ⊥ ≤
    Finset.card.{u_7} (α := ?m.38 (H := ⊥)) (sorry : Finset (?m.38 (H := ⊥)))
inr :
  ∀ (hH : H ≠ ⊥),
    #G.edgeFinset - G.copyCount H ≤ Finset.card.{u_7} (α := ?m.38 (H := H)) (sorry : Finset (?m.38 (H := H)))
⊢ #G.edgeFinset - G.copyCount H ≤ Finset.card.{u_7} (α := ?m.38 (H := H)) (sorry : Finset (?m.38 (H := H)))

Tactic:
obtain rfl | hH := eq_or_ne H ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
inl :
  Fintype.card.{u_1} (↑G.edgeSet : Type u_1) - copyCount.{u_1, u_2} (W := W) G ⊥ ≤
    Finset.card.{u_7} (α := ?m.38 (H := ⊥)) (sorry () : Finset (?m.38 (H := ⊥)))
⊢ #G.edgeFinset - copyCount.{u_1, u_2} (W := W) G ⊥ ≤
    Finset.card.{u_7} (α := ?m.38 (H := ⊥)) (sorry : Finset (?m.38 (H := ⊥)))

Tactic:
simp [← card_edgeSet]

Premises used: SimpleGraph.card_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
hH : H ≠ ⊥
f : (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) → Sym2 V :=
  fun (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) ↦ ⋯.some (s := (↑G' : G.Subgraph).edgeSet)
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card.{u_1} { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
hH : H ≠ ⊥
f : (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) → Sym2 V :=
  fun (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) ↦ ⋯.some (s := (↑G' : G.Subgraph).edgeSet)
⊢ #G.edgeFinset - Fintype.card.{u_1} { G' : G.Subgraph // Nonempty (H ≃g G'.coe) } ≤ #G.edgeFinset - #(image f univ)

Tactic:
Nat.sub_le_sub_left card_image_le _

Premises used: Nat.sub_le_sub_left, Fintype.card, Finset.card_image_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
hH : H ≠ ⊥
f : (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) → Sym2 V :=
  fun (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) ↦ ⋯.some (s := (↑G' : G.Subgraph).edgeSet)
rw rw₁ : #G.edgeFinset - #(image f univ) = #G.edgeFinset - #(image f univ)
⊢ #G.edgeFinset - #(image f univ) = #G.edgeFinset - #(Set.range f).toFinset

Tactic:
rw [Set.toFinset_range]

Premises used: Set.toFinset_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
hH : H ≠ ⊥
f : (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) → Sym2 V :=
  fun (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) ↦ ⋯.some (s := (↑G' : G.Subgraph).edgeSet)
⊢ #G.edgeFinset - #(Set.range f).toFinset ≤ #(G.edgeFinset \ (Set.range f).toFinset)

Tactic:
le_card_sdiff ..

Premises used: Finset.le_card_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
hH : H ≠ ⊥
f : (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) → Sym2 V :=
  fun (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) ↦ ⋯.some (s := (↑G' : G.Subgraph).edgeSet)
⊢ #(G.edgeFinset \ (Set.range f).toFinset) = Finset.card (α := ?m.145) sorry

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ H ≠ ⊥

Tactic:
classical
  obtain rfl | hH := eq_or_ne H ⊥
  · simp [← card_edgeSet]
  let f (G' : {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}) := (aux hH G'.2).some
  calc
    _ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
    _ ≤ #G.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
    _ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
    _ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
    _ = #(G.killCopies H).edgeFinset := ?_
  · simp only [edgeFinset, Set.toFinset_card]
    rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
  congr 1
  ext e
  induction e using Sym2.inductionOn with | hf v w
  simp [mem_edgeSet, killCopies_of_ne_bot hH, f, eq_comm]

Premises used: Finset.card_univ, Nat.sub_le_sub_left, Bot.bot, Set.toFinset_card, eq_comm, SimpleGraph.copyCount, SimpleGraph.edgeFinset, Finset.card_image_le, Finset.le_card_sdiff, eq_or_ne, Finset.card_subtype, SimpleGraph.card_edgeSet, SimpleGraph.mem_edgeSet, Finset.subtype_univ, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset ≤ #sorry + G.copyCount H

Tactic:
tsub_le_iff_right.1 le_card_edgeFinset_killCopies

Premises used: Unit.unit, sorryAx, Lean.Name.num, tsub_le_iff_right, Lean.Name.str, Lean.Name.anonymous, Bool.true, Iff.mp, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d₁ d₂ : G.Dart
mk :
  ∀ (toProd : V × V) (adj : G.Adj toProd.1 toProd.2),
    { toProd := toProd, adj := adj : G.Dart } = d₂ ↔ { toProd := toProd, adj := adj : G.Dart }.toProd = d₂.toProd
⊢ d₁ = d₂ ↔ d₁.toProd = d₂.toProd

Tactic:
cases d₁
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
toProd : V × V
adj : G.Adj toProd.1 toProd.2
mk :
  ∀ (toProd_1 : V × V) (adj_1 : G.Adj toProd_1.1 toProd_1.2),
    { toProd := toProd, adj := adj : G.Dart } = { toProd := toProd_1, adj := adj_1 } ↔
      { toProd := toProd, adj := adj : G.Dart }.toProd = { toProd := toProd_1, adj := adj_1 : G.Dart }.toProd
⊢ { toProd := toProd, adj := adj : G.Dart } = d₂ ↔ { toProd := toProd, adj := adj : G.Dart }.toProd = d₂.toProd

Tactic:
cases d₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
toProd : V × V
adj : G.Adj toProd.1 toProd.2
toProd_1 : V × V
adj_1 : G.Adj toProd_1.1 toProd_1.2
⊢ { toProd := toProd, adj := adj : G.Dart } = { toProd := toProd_1, adj := adj_1 } ↔
    { toProd := toProd, adj := adj : G.Dart }.toProd = { toProd := toProd_1, adj := adj_1 : G.Dart }.toProd

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d₁ d₂ : G.Dart
h : d₁.toProd = d₂.toProd
⊢ d₁ = d₂

Tactic:
(Dart.ext_iff d₁ d₂).mpr h

Premises used: Iff.mpr, SimpleGraph.Dart.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.toProd.1 ≠ d.toProd.2

Tactic:
fun h ↦ G.irrefl (h ▸ d.adj)

Premises used: SimpleGraph.irrefl, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.toProd.2 ≠ d.toProd.1

Tactic:
fun h ↦ G.irrefl (h ▸ d.adj)

Premises used: SimpleGraph.irrefl, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := G.Dart) toProd

Tactic:
Dart.ext

Premises used: SimpleGraph.Dart.ext, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
⊢ { toProd := p, adj := h : G.Dart }.edge = s(p.1, p.2)

Tactic:
rfl

Premises used: SimpleGraph.Dart.edge, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.edge ∈ G.edgeSet

Tactic:
d.adj

Premises used: Set.Mem, setOf, Sym2.fromRel, SimpleGraph.Dart.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
⊢ { toProd := p, adj := h : G.Dart }.symm = { toProd := p.swap, adj := ⋯ }

Tactic:
rfl

Premises used: SimpleGraph.Dart.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.symm.edge = d.edge

Tactic:
Sym2.eq_swap

Premises used: Sym2.eq_swap, SimpleGraph.Dart.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Eq.{u_1 + 1} (α := G.Dart → Sym2 V) (edge ∘ symm) edge

Tactic:
funext Dart.edge_symm

Premises used: SimpleGraph.Dart.edge_symm, funext
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.symm.symm = d

Tactic:
Dart.ext _ _ <| Prod.swap_swap _

Premises used: Prod.swap_swap, SimpleGraph.Dart.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Function.Involutive.{u_1 + 1} (α := G.Dart) symm

Tactic:
Dart.symm_symm

Premises used: SimpleGraph.Dart.symm_symm, Function.Involutive
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
d : G.Dart
⊢ d.symm ≠ d

Tactic:
ne_of_apply_ne (Prod.snd ∘ Dart.toProd) d.adj.ne

Premises used: SimpleGraph.Adj.ne, Function.comp, ne_of_apply_ne, SimpleGraph.Dart.toProd, SimpleGraph.Dart.adj, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
p : V × V
hp : G.Adj p.1 p.2
q : V × V
hq : G.Adj q.1 q.2
⊢ { toProd := p, adj := hp : G.Dart }.edge = { toProd := q, adj := hq : G.Dart }.edge ↔
    { toProd := p, adj := hp : G.Dart } = { toProd := q, adj := hq } ∨
      { toProd := p, adj := hp : G.Dart } = { toProd := q, adj := hq }.symm

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
u v : V
⊢ { toProd := p, adj := h : G.Dart }.edge = s(u, v) ↔
    { toProd := p, adj := h : G.Dart }.toProd = (u, v) ∨ { toProd := p, adj := h : G.Dart }.toProd = (v, u)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
rw :
  { fst := a, snd := b, adj := h : G.Dart }.toProd = (u, v) ∨
      { fst := a, snd := b, adj := h : G.Dart }.toProd = (v, u) ↔
    { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = u ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = v ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = u
⊢ { fst := a, snd := b, adj := h : G.Dart }.edge = s(u, v) ↔
    { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = u ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = v ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = u

Tactic:
rw [dart_edge_eq_mk'_iff]

Premises used: SimpleGraph.dart_edge_eq_mk'_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
a b : V
h : G.Adj (a, b).1 (a, b).2
u v : V
⊢ { fst := a, snd := b, adj := h : G.Dart }.toProd = (u, v) ∨
      { fst := a, snd := b, adj := h : G.Dart }.toProd = (v, u) ↔
    { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = u ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = v ∨
      { fst := a, snd := b, adj := h : G.Dart }.toProd.1 = v ∧ { fst := a, snd := b, adj := h : G.Dart }.toProd.2 = u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : (↑(G.neighborSet v) : Type u_1)
h : G.dartOfNeighborSet v e₁ = G.dartOfNeighborSet v e₂
⊢ (v, (↑e₁ : V)) = (v, (↑e₂ : V))

Tactic:
injection h with h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : (↑(G.neighborSet v) : Type u_1)
h' : (v, (↑e₁ : V)) = (v, (↑e₂ : V))
⊢ (v, (↑e₁ : V)).2 = (v, (↑e₂ : V)).2

Tactic:
congr_arg Prod.snd h'

Premises used: congr_arg, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : (↑(G.neighborSet v) : Type u_1)
h' : (v, (↑e₁ : V)) = (v, (↑e₂ : V))
⊢ (↑e₁ : V) = (↑e₂ : V)

Tactic:
convert! congr_arg Prod.snd h'

Premises used: congr_arg, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nontrivial V
obtain : ∀ (v w : V) (h : v ≠ w), Nonempty.{u_1 + 1} (Dart (V := V) ⊤)
⊢ Nonempty.{u_1 + 1} (Dart (V := V) ⊤)

Tactic:
obtain ⟨v, w, h⟩ := exists_pair_ne V

Premises used: exists_pair_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nontrivial V
v w : V
h : v ≠ w
⊢ Nonempty.{u_1 + 1} (Dart (V := V) ⊤)

Tactic:
⟨⟨(v, w), h⟩⟩

Premises used: Prod.mk, Nonempty.intro, SimpleGraph.Dart.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Dart
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nontrivial V
v w : V
h : v ≠ w
⊢ Nonempty.{u_1 + 1} (Dart (V := V) ⊤)

Tactic:
exact ⟨⟨(v, w), h⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
h :
  ∀ (d : G.Dart),
    Membership.mem (γ := Finset G.Dart) {d : G.Dart | d.toProd.1 = v} d ↔ d ∈ image (G.dartOfNeighborSet v) univ
⊢ {d : G.Dart | d.toProd.1 = v} = image (G.dartOfNeighborSet v) univ

Tactic:
ext d
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
d : G.Dart
h :
  d.toProd.1 = v ↔
    ∃ (x : V) (h : x ∈ G.neighborSet v),
      G.dartOfNeighborSet v (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) x h) = d
⊢ Membership.mem (γ := Finset G.Dart) {d : G.Dart | d.toProd.1 = v} d ↔ d ∈ image (G.dartOfNeighborSet v) univ

Tactic:
simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]

Premises used: Finset.mem_univ, Finset.mem_image, SetCoe.exists, Finset.mem_filter, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
d : G.Dart
h :
  d.toProd.1 = v →
    ∃ (x : V) (h : x ∈ G.neighborSet v),
      G.dartOfNeighborSet v (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) x h) = d
h₁ :
  (∃ (x : V) (h : x ∈ G.neighborSet v),
      G.dartOfNeighborSet v (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) x h) = d) →
    d.toProd.1 = v
⊢ d.toProd.1 = v ↔
    ∃ (x : V) (h : x ∈ G.neighborSet v),
      G.dartOfNeighborSet v (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) x h) = d

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
h :
  (G.dartOfNeighborSet d.toProd.1
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯)).toProd.1 =
    d.toProd.1
h₁ :
  (G.dartOfNeighborSet d.toProd.1
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯)).toProd.2 =
    d.toProd.2
⊢ G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯) = d

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
⊢ (G.dartOfNeighborSet d.toProd.1
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯)).toProd.1 =
    d.toProd.1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
⊢ (G.dartOfNeighborSet d.toProd.1
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯)).toProd.2 =
    d.toProd.2

Tactic:
rfl