awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced
have mp : (Subgraph.map f.toHom ⊤).IsInduced
Tactic: refine ⟨Subgraph.map f.toHom ⊤, f.toCopy.isoToSubgraph, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : Fintype W
inst_2 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ G.labelledCopyCount H = 1
have convert_2 : Unique (H.Copy G)
Tactic: convert! Fintype.card_unique
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
⊢ Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)} =
    Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ)
have e_s : Eq.{u_1 + 1} (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
  (image (α := H.Copy G) Copy.toSubgraph univ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype { f : H →g G // Injective.{u_2 + 1, u_1 + 1} (α := W) (β := V) (⇑f : (a : W) → V) }
inst_2 : DecidableEq G.Subgraph
⊢ Eq.{u_1 + 1} (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
    (image (α := H.Copy G) Copy.toSubgraph univ)
have e_s : (↑{G' : G.Subgraph | Nonempty (H ≃g G'.coe)} : Set G.Subgraph) =
  (↑(image (α := H.Copy G) Copy.toSubgraph univ) : Set G.Subgraph)
Tactic: refine Finset.coe_injective ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ G.copyCount H ≤ G.labelledCopyCount H
have rw : Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H
Tactic: rw [copyCount_eq_card_image_copyToSubgraph]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
⊢ G.copyCount H ≤ G.labelledCopyCount H
have classical : Finset.card.{u_1} (α := G.Subgraph) (image (α := H.Copy G) Copy.toSubgraph univ) ≤ G.labelledCopyCount H
Tactic: classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)} = 1
have h : Eq (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)}
  {{ verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }}
Tactic: convert!
    card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ 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 := ⋯ }}
have h : Nonempty.{u_1 + 1}
    (Iso (V := V) (W := (↑Set.univ : Type u_1)) ⊥
      (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry } :
        SimpleGraph
          (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }) :
            Type u_1))) ∧
  ∀ (x : G.Subgraph) (a : Iso (V := V) ⊥ x.coe),
    x = { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }
Tactic: simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ 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 := ⋯ }
have h : ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe),
  H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }
Tactic: 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) ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
H' : G.Subgraph
e : Iso (V := V) ⊥ H'.coe
⊢ H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
have h : ∀ (a b : V),
  H'.Adj a b ↔ Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry } a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
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
have h : ¬H'.Adj a b
Tactic: simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
⊢ G.copyCount (W := V) ⊥ = 1
have rw : Finset.card.{u_1} (α := G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)} = 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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
⊢ G.copyCount (W := V) ⊥ = 1
have h : Eq (α := Finset G.Subgraph) {G' : G.Subgraph | Nonempty.{u_1 + 1} (Iso (V := V) ⊥ G'.coe)}
  {{ verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }}
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 := ⋯ }}
⊢ G.copyCount (W := V) ⊥ = 1
have h₁ : Nonempty.{u_1 + 1}
    (Iso (V := V) (W := (↑Set.univ : Type u_1)) ⊥
      (Subgraph.coe { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry } :
        SimpleGraph
          (↑(Subgraph.verts (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }) :
            Type u_1))) ∧
  ∀ (x : G.Subgraph) (a : Iso (V := V) ⊥ x.coe),
    x = { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 := ⋯ }
⊢ G.copyCount (W := V) ⊥ = 1
have h₂ : ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe),
  H'.Adj = Subgraph.Adj (G := G) { verts := Set.univ, Adj := ⊥, adj_sub := sorry, edge_vert := sorry, symm := sorry }
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 := ⋯ }
⊢ G.copyCount (W := V) ⊥ = 1
have 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 := sorry, edge_vert := sorry, symm := sorry } a b
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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
⊢ G.copyCount (W := V) ⊥ = 1
have h₄ : ∀ (H' : G.Subgraph) (e : Iso (V := V) ⊥ H'.coe) (a b : V), ¬H'.Adj a b
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
inst_1 : IsEmpty W
G : SimpleGraph V
H : SimpleGraph W
⊢ G.copyCount H = 1
have intro : ∀ (val : Fintype W), G.copyCount H = 1
Tactic: cases nonempty_fintype W
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
⊢ Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty
have obtain : ∀ (e : Sym2 W) (he : e ∈ H.edgeSet), Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty
Tactic: obtain ⟨e, he⟩ := edgeSet_nonempty.2 hH
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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) → G'.edgeSet.Nonempty
have rw : Nonempty (H ≃g G'.coe) → (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' G'.coe.edgeSet).Nonempty
Tactic: rw [← Subgraph.image_coe_edgeSet_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ sorry = G ↔ H.Free G
have simp : sorry = G ↔ ∀ (x : G.Subgraph), IsEmpty (H ≃g x.coe)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
⊢ sorry = G
have inl : ∀ (hHG : Free.{u_2, u_1} (α := W) ⊥ G), sorry = G
Tactic: obtain rfl | hH := eq_or_ne H ⊥
Cleared hypotheses: H, hHG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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
⊢ sorry = G
have inr : ∀ (hH : H ≠ ⊥), sorry = G
Tactic: obtain rfl | hH := eq_or_ne H ⊥
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 - G.copyCount H ≤ Finset.card.{u_7} (α := ?m.38 (H := H)) (sorry : Finset (?m.38 (H := H)))
have inl : #G.edgeFinset - copyCount.{u_1, u_2} (W := W) G ⊥ ≤
  Finset.card.{u_7} (α := ?m.38 (H := ⊥)) (sorry : Finset (?m.38 (H := ⊥)))
Tactic: obtain rfl | hH := eq_or_ne H ⊥
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 := ⊥)))
⊢ #G.edgeFinset - G.copyCount H ≤ Finset.card.{u_7} (α := ?m.38 (H := H)) (sorry : Finset (?m.38 (H := H)))
have inr : ∀ (hH : 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 ⊥
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset - copyCount.{u_1, u_2} (W := W) G ⊥ ≤
    Finset.card.{u_7} (α := ?m.38 (H := ⊥)) (sorry : Finset (?m.38 (H := ⊥)))
have 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 := ⊥)))
Tactic: simp [← card_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (goal)
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 - #(image f univ) = #G.edgeFinset - #(Set.range f).toFinset
have rw : #G.edgeFinset - #(image f univ) = #G.edgeFinset - #(image f univ)
Tactic: rw [Set.toFinset_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Copy (hypothesis)
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 - G.copyCount H ≤ #sorry
have hH : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Dart (goal)
Goal:
V : Type u_1
G : SimpleGraph V
d₁ d₂ : G.Dart
⊢ d₁ = d₂ ↔ d₁.toProd = d₂.toProd
have 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
Tactic: cases d₁
Cleared hypotheses: d₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Dart (goal)
Goal:
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
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
have 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
Tactic: cases d₂
Cleared hypotheses: d₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Dart (goal)
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 }.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
have 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
Tactic: rw [dart_edge_eq_mk'_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Dart (hypothesis)
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₂
⊢ (↑e₁ : V) = (↑e₂ : V)
have h' : (v, (↑e₁ : V)) = (v, (↑e₂ : V))
Tactic: injection h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Dart (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nontrivial V
⊢ Nonempty.{u_1 + 1} (Dart (V := V) ⊤)
have obtain : ∀ (v w : V) (h : v ≠ w), Nonempty.{u_1 + 1} (Dart (V := V) ⊤)
Tactic: obtain ⟨v, w, h⟩ := exists_pair_ne V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
⊢ {d : G.Dart | d.toProd.1 = v} = image (G.dartOfNeighborSet v) univ
have h : ∀ (d : G.Dart),
  Membership.mem (γ := Finset G.Dart) {d : G.Dart | d.toProd.1 = v} d ↔ d ∈ image (G.dartOfNeighborSet v) univ
Tactic: ext d
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
d : G.Dart
⊢ Membership.mem (γ := Finset G.Dart) {d : G.Dart | d.toProd.1 = v} d ↔ d ∈ image (G.dartOfNeighborSet v) univ
have 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
Tactic: simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
d : G.Dart
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ 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
have 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
Tactic: constructor