awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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)
⊢ map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset (↑v : V)
have 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)
Tactic: classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ (induce s G).degree v = G.degree (↑v : V)
have simp_rw : #((induce s G).neighborFinset v) = #(G.neighborFinset (↑v : V))
Tactic: simp_rw [← card_neighborFinset_eq_degree,
    ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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))
⊢ (induce s G).degree v = G.degree (↑v : V)
have simp_rw₁ : #((induce s G).neighborFinset v) = #(map (Embedding.subtype fun (x : V) ↦ x ∈ s) ((induce s G).neighborFinset v))
Tactic: simp_rw [← card_neighborFinset_eq_degree,
    ← map_neighborFinset_induce_of_neighborSet_subset h, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G) = map f.sym2Map G.edgeFinset
have rw : (↑(edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) : Set (Sym2 W)) = (↑(map f.sym2Map G.edgeFinset) : Set (Sym2 W))
Tactic: rw [← Finset.coe_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ (↑(edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) : Set (Sym2 W)) = (↑(map f.sym2Map G.edgeFinset) : Set (Sym2 W))
have 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)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ card.{u_2} (α := Sym2 W) (edgeFinset (SimpleGraph.map (⇑f : (a : V) → W) G)) = #G.edgeFinset
have rw : #(map f.sym2Map G.edgeFinset) = #G.edgeFinset
Tactic: rw [edgeFinset_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨆ (i : ι), f i) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))
have rw : Eq.{u + 1} (α := G.Subgraph) (↑(sSup (range fun (i : ι) ↦ f i)) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))
Tactic: rw [iSup, coe_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨆ (i : ι), f i) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))
have 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))
Tactic: rw [iSup, coe_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨆ (i : ι), f i) : G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph))
have rw₂ : Eq.{u + 1} (α := G.Subgraph) (⨆ (i : ι), (↑(f i) : G.Subgraph)) (⨆ (i : ι), (↑(f i) : G.Subgraph))
Tactic: rw [iSup, coe_sSup, iSup_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨅ (i : ι), f i) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))
have rw : Eq.{u + 1} (α := G.Subgraph) (↑(sInf (range fun (i : ι) ↦ f i)) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))
Tactic: rw [iInf, coe_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨅ (i : ι), f i) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))
have 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))
Tactic: rw [iInf, coe_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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))
⊢ Eq.{u + 1} (α := G.Subgraph) (↑(⨅ (i : ι), f i) : G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph))
have rw₂ : Eq.{u + 1} (α := G.Subgraph) (⨅ (i : ι), (↑(f i) : G.Subgraph)) (⨅ (i : ι), (↑(f i) : G.Subgraph))
Tactic: rw [iInf, coe_sInf, iInf_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : G.Finsubgraph
h : G'' ≤ G'
f : G' →fg F
⊢ G'' →fg F
have 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 sorry) :
            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 sorry) :
            W))
        b)
Tactic: refine ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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
⊢ Nonempty (G →g F)
have intro : ∀ (val : Fintype W), Nonempty (G →g F)
Tactic: cases nonempty_fintype W
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (hypothesis)
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
⊢ Nonempty (G →g F)
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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ᵒᵖ
⊢ Fintype ((G.finsubgraphHomFunctor F).obj G')
have haveI : (this : Fintype (↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u)) → Fintype ((G.finsubgraphHomFunctor F).obj G')
Tactic: haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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 ((G.finsubgraphHomFunctor F).obj G')
have haveI : (this : Fintype ((↑(↑(Opposite.unop G') : G.Subgraph).verts : Type u) → W)) →
  Fintype ((G.finsubgraphHomFunctor F).obj G')
Tactic: haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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')
⊢ Nonempty (G →g F)
have intro : ∀ (this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')), 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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')
⊢ Nonempty (G →g F)
have intro : ∀ (u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j) (hu : u ∈ (G.finsubgraphHomFunctor F).sections),
  Nonempty (G →g F)
Tactic: obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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)
have intro : (v : V) → W
Tactic: refine ⟨⟨fun v => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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
⊢ Nonempty (G →g F)
have 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 sorry))
        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 sorry))
        b)
Tactic: refine ⟨⟨fun v => ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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
e : G.Adj v v'
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
have intro : ∀ (hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)),
  F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v sorry))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' sorry))
Tactic: have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
have intro : ∀ (hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')),
  F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v sorry))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' sorry))
Tactic: have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)