awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
v : (↑s : Type u_1)
h : G.neighborSet (↑v : V) ⊆ s
rwa :
  ∀ (h : (G.neighborSet (↑v : V)).toFinset ⊆ s.toFinset),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₁ :
  ∀ (h : G.neighborFinset (↑v : V) ⊆ s.toFinset),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₂ :
  ∀ (h : G.neighborFinset (↑v : V) ∩ s.toFinset = G.neighborFinset (↑v : V)),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (h : map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)

Tactic:
rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h

Premises used: SimpleGraph.map_neighborFinset_induce, Finset.inter_eq_left, Set.toFinset_subset_toFinset, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
v : (↑s : Type u_1)
h : G.neighborSet (↑v : V) ⊆ s
rwa :
  ∀ (h : (G.neighborSet (↑v : V)).toFinset ⊆ s.toFinset),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₁ :
  ∀ (h : G.neighborFinset (↑v : V) ⊆ s.toFinset),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₂ :
  ∀ (h : G.neighborFinset (↑v : V) ∩ s.toFinset = G.neighborFinset (↑v : V)),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (h : map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)),
    map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)

Tactic:
classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h

Premises used: Finset.inter_eq_left, Set.toFinset_subset_toFinset, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
v : (↑s : Type u_1)
h : G.neighborSet (↑v : V) ⊆ s
simp_rw : #((induce s G).neighborFinset v) = #(G.neighborFinset (↑v : V))
simp_rw₁ :
  #((induce s G).neighborFinset v) = #(map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v))
⊢ (induce s G).degree v = G.degree (↑v : V)

Tactic:
simp_rw [← card_neighborFinset_eq_degree,
    ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]

Premises used: Finset.card_map, SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset, SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
s : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ s
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.support ⊆ s
v : (↑s : Type u_1)
⊢ (induce s G).degree v = G.degree (↑v : V)

Tactic:
degree_induce_of_neighborSet_subset <| (G.neighborSet_subset_support v).trans h

Premises used: HasSubset.Subset.trans, SimpleGraph.degree_induce_of_neighborSet_subset, SimpleGraph.neighborSet_subset_support, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
v : (↑G.support : Type u_1)
⊢ (induce G.support G).degree v = G.degree (↑v : V)

Tactic:
degree_induce_of_support_subset subset_rfl v

Premises used: SimpleGraph.degree_induce_of_support_subset, subset_rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
rw :
  (↑(edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) : Set (Sym2 W)) = (↑(map f.sym2Map G.edgeFinset) : Set (Sym2 W))
⊢ edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G) = map f.sym2Map G.edgeFinset

Tactic:
rw [← Finset.coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
push_cast :
  Eq.{u_2 + 1} (α := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G))
    ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet)
⊢ (↑(edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) : Set (Sym2 W)) = (↑(map f.sym2Map G.edgeFinset) : Set (Sym2 W))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
⊢ Eq.{u_2 + 1} (α := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G))
    ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet)

Tactic:
G.edgeSet_map f

Premises used: SimpleGraph.edgeSet_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
⊢ Eq.{u_2 + 1} (α := Set (Sym2 W)) (edgeSet (SimpleGraph.map (⇑f : (a : V) → W) G))
    ((⇑f.sym2Map : (a : Sym2 V) → Sym2 W) '' G.edgeSet)

Tactic:
exact G.edgeSet_map f

Premises used: SimpleGraph.edgeSet_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
rw : #(map f.sym2Map G.edgeFinset) = #G.edgeFinset
⊢ card.{u_2} (α := Sym2 W) (edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) = #G.edgeFinset

Tactic:
rw [edgeFinset_map]

Premises used: SimpleGraph.edgeFinset_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
⊢ #(map f.sym2Map G.edgeFinset) = #G.edgeFinset

Tactic:
G.edgeFinset.card_map f.sym2Map

Premises used: Finset.card_map, Function.Embedding.sym2Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
inst_1 : Fintype W
inst_2 : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst_3 : DecidableRel G.Adj
⊢ #(map f.sym2Map G.edgeFinset) = #G.edgeFinset

Tactic:
exact G.edgeFinset.card_map f.sym2Map

Premises used: Finset.card_map, Function.Embedding.sym2Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := G.Subgraph) (↑⊥ : G.Subgraph) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Finsubgraph
⊢ (↑(G₁ ⊔ G₂) : G.Subgraph) = (↑G₁ : G.Subgraph) ⊔ (↑G₂ : G.Subgraph)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Finsubgraph
⊢ (↑(G₁ ⊓ G₂) : G.Subgraph) = (↑G₁ : G.Subgraph) ⊓ (↑G₂ : G.Subgraph)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Finsubgraph
⊢ (↑(G₁ \ G₂) : G.Subgraph) = (↑G₁ : G.Subgraph) \ (↑G₂ : G.Subgraph)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
⊢ Eq.{u + 1} (α := G.Subgraph) (↑⊤ : G.Subgraph) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : G.Finsubgraph
⊢ (↑G'ᶜ : G.Subgraph) = (↑G' : G.Subgraph)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : G.Finsubgraph
⊢ (↑(￢G') : G.Subgraph) = ￢(↑G' : G.Subgraph)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G₁ G₂ : G.Finsubgraph
⊢ (↑(G₁ ⇨ G₂) : G.Subgraph) = (↑G₁ : G.Subgraph) ⇨ (↑G₂ : G.Subgraph)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
s : Set G.Finsubgraph
⊢ (↑(sSup s) : G.Subgraph) = ⨆ G_1 ∈ s, (↑G_1 : G.Subgraph)

Tactic:
rfl

Premises used: iSup, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
s : Set G.Finsubgraph
⊢ (↑(sInf s) : G.Subgraph) = ⨅ G_1 ∈ s, (↑G_1 : G.Subgraph)

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
rw : Eq.{u + 1} (α := G.Subgraph) (↑(sSup (range fun (i : ι) ↦ f i)) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))
rw₁ :
  Eq.{u + 1} (α := G.Subgraph)
    (⨆ (G_1 : G.Finsubgraph),
      ⨆ (_ : Membership.mem (γ := Set G.Finsubgraph) (range fun (i : ι) ↦ f i) G_1), (↑G_1 : G.Subgraph))
    (⨆ (i : ι), (↑(f i) : G.Subgraph))
rw₂ rw₃ : Eq.{u + 1} (α := G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph)) (⨆ (i : ι), (↑(f i) : G.Subgraph))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨆ (i : ι), f i) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))

Tactic:
rw [iSup, coe_sSup, iSup_range]

Premises used: SimpleGraph.Finsubgraph.coe_sSup, iSup, iSup_range
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
rw : Eq.{u + 1} (α := G.Subgraph) (↑(sInf (range fun (i : ι) ↦ f i)) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))
rw₁ :
  Eq.{u + 1} (α := G.Subgraph)
    (⨅ (G_1 : G.Finsubgraph),
      ⨅ (_ : Membership.mem (γ := Set G.Finsubgraph) (range fun (i : ι) ↦ f i) G_1), (↑G_1 : G.Subgraph))
    (⨅ (i : ι), (↑(f i) : G.Subgraph))
rw₂ rw₃ : Eq.{u + 1} (α := G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph)) (⨅ (i : ι), (↑(f i) : G.Subgraph))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨅ (i : ι), f i) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))

Tactic:
rw [iInf, coe_sInf, iInf_range]

Premises used: iInf, iInf_range, SimpleGraph.Finsubgraph.coe_sInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
v : V
⊢ (G.singletonSubgraph v).verts.Finite

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : G.Adj u v
⊢ (G.subgraphOfAdj e).verts.Finite

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

Premises used: SimpleGraph.singletonFinsubgraph, SimpleGraph.finsubgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

Premises used: SimpleGraph.singletonFinsubgraph, SimpleGraph.finsubgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : G.Finsubgraph
h : G'' ≤ G'
f : G' →fg F
refine :
  ∀ {a b : (↑(↑G'' : G.Subgraph).verts : Type u)},
    (↑G'' : G.Subgraph).coe.Adj a b →
      F.Adj
        ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
            (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
              | ⟨v, hv⟩ =>
                f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
                  (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
              W))
          a)
        ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
            (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
              | ⟨v, hv⟩ =>
                f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
                  (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
              W))
          b)
⊢ G'' →fg F

Tactic:
refine ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : G.Finsubgraph
h : G'' ≤ G'
f : G' →fg F
u : V
hu : u ∈ (↑G'' : G.Subgraph).verts
v : V
hv : v ∈ (↑G'' : G.Subgraph).verts
huv :
  (↑G'' : G.Subgraph).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) u hu)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) v hv)
⊢ F.Adj
    ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
        (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
          | ⟨v, hv⟩ =>
            f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
          W))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) u hu))
    ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
        (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
          | ⟨v, hv⟩ =>
            f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
          W))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) v hv))

Tactic:
f.map_rel' (h.2 huv)

Premises used: RelHom.map_rel', And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : G.Finsubgraph
h : G'' ≤ G'
f : G' →fg F
u : V
hu : u ∈ (↑G'' : G.Subgraph).verts
v : V
hv : v ∈ (↑G'' : G.Subgraph).verts
huv :
  (↑G'' : G.Subgraph).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) u hu)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) v hv)
⊢ F.Adj
    ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
        (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
          | ⟨v, hv⟩ =>
            f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
          W))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) u hu))
    ((fun (x : (↑(↑G'' : G.Subgraph).verts : Type u)) ↦
        (match (motive := (↑(↑G'' : G.Subgraph).verts : Type u) → W) x with
          | ⟨v, hv⟩ =>
            f.toFun (r := (↑G' : G.Subgraph).coe.Adj) (s := F.Adj)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G' : G.Subgraph).verts) v ⋯) :
          W))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑G'' : G.Subgraph).verts) v hv))

Tactic:
exact f.map_rel' (h.2 huv)
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
intro : ∀ (val : Fintype W), Nonempty (G →g F)
⊢ Nonempty (G →g F)

Tactic:
cases nonempty_fintype W

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
⊢ ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')

Tactic:
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' =>
    ⟨h G'.unop G'.unop.property⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
haveI :
  (this : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)) → Fintype ((G.finsubgraphHomFunctor F).obj G')
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)
⊢ Fintype ((↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u) → W)

Tactic:
exact Pi.instFintype

Premises used: Pi.instFintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)
⊢ Fintype ((↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u) → W)

Tactic:
classical exact Pi.instFintype

Premises used: Pi.instFintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)
haveI :
  (this : Fintype ((↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u) → W)) →
    Fintype ((G.finsubgraphHomFunctor F).obj G')
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
G' : G.Finsubgraphᵒᵖ
this_2 : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)
this : Fintype ((↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u) → W)
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')

Tactic:
exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective

Premises used: Fintype.ofInjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
intro : ∀ (this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')), Nonempty (G →g F)
⊢ Nonempty (G →g F)

Tactic:
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') := by
    intro G'
    haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
    haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
    exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
intro :
  ∀ (u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j) (hu : u ∈ (G.finsubgraphHomFunctor F).sections),
    Nonempty (G →g F)
⊢ Nonempty (G →g F)

Tactic:
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)

Premises used: SimpleGraph.finsubgraphHomFunctor, nonempty_sections_of_finite_inverse_system
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ Nonempty (G →g F)

Tactic:
⟨⟨fun v => ?_, ?_⟩⟩

Premises used: Nonempty.intro, RelHom.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
intro : (v : V) → W
intro₁ :
  ∀ {a b : V},
    G.Adj a b →
      F.Adj
        ((fun (v : V) ↦
            RelHom.toFun (r :=
              Adj (Subgraph.coe (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph))) (s := F.Adj)
              (u (Opposite.op (singletonFinsubgraph v)))
              (Subtype.mk (p := fun (x : V) ↦
                x ∈ Subgraph.verts (G := G) (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)) v
                ⋯))
          a)
        ((fun (v : V) ↦
            RelHom.toFun (r :=
              Adj (Subgraph.coe (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph))) (s := F.Adj)
              (u (Opposite.op (singletonFinsubgraph v)))
              (Subtype.mk (p := fun (x : V) ↦
                x ∈ Subgraph.verts (G := G) (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)) v
                ⋯))
          b)
⊢ Nonempty (G →g F)

Tactic:
refine ⟨⟨fun v => ?_, ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ v ∈
    (↑(Opposite.unop
            (Opposite.op (Subtype.mk (p := fun (G' : G.Subgraph) ↦ G'.verts.Finite) (G.singletonSubgraph v) ⋯))) :
        G.Subgraph).verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ W

Tactic:
exact
      (u (Opposite.op (singletonFinsubgraph v))).toFun
        ⟨v, by
          unfold singletonFinsubgraph
          simp⟩

Premises used: SimpleGraph.singletonFinsubgraph, RelHom.toFun, Subtype.mk, Opposite.op