awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' = ⊥
have mp : ∀ (x : V), x ∈ M'.verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊥) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
mp : ∀ (x : V), x ∈ M'.verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊥) x
⊢ M' = ⊥
have mp₁ : ∀ (x x_1 : V), M'.Adj x x_1 ↔ Adj (G := G) ⊥ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
⊢ M' ≤ M
have left : M'.verts ⊆ M.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
left : M'.verts ⊆ M.verts
⊢ M' ≤ M
have right : ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ Membership.mem (γ := Set V) ⊥ v
have hle : ∀ {M : G.Subgraph} (h : v ∈ M.verts), M' ≤ M
Tactic: have hle {M : Subgraph G} (h : v ∈ M.verts) : M' ≤ M := by constructor <;> simp [h, M']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ Subgraph.map Hom.id H = H
have verts : ∀ (x : V), x ∈ (Subgraph.map Hom.id H).verts ↔ x ∈ H.verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
verts : ∀ (x : V), x ∈ (Subgraph.map Hom.id H).verts ↔ x ∈ H.verts
⊢ Subgraph.map Hom.id H = H
have Adj : ∀ (x x_1 : V), (Subgraph.map Hom.id H).Adj x x_1 ↔ H.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)
have verts : ∀ (x : U), x ∈ (Subgraph.map (g.comp f) H).verts ↔ x ∈ (Subgraph.map g (Subgraph.map f H)).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
verts : ∀ (x : U), x ∈ (Subgraph.map (g.comp f) H).verts ↔ x ∈ (Subgraph.map g (Subgraph.map f H)).verts
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)
have Adj : ∀ (x x_1 : U), (Subgraph.map (g.comp f) H).Adj x x_1 ↔ (Subgraph.map g (Subgraph.map f H)).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ Subgraph.map f H₁ ≤ Subgraph.map f H₂
have left : (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
left : (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts
⊢ Subgraph.map f H₁ ≤ Subgraph.map f H₂
have right : ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a : W
⊢ a ∈ (Subgraph.map f H₁).verts → a ∈ (Subgraph.map f H₂).verts
have left : ∀ x ∈ H₁.verts, (f : (a : V) → W) x = a → ∃ x ∈ H₂.verts, (f : (a : V) → W) x = a
Tactic: simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
⊢ Subgraph.map f (H₁ ⊔ H₂) = Subgraph.map f H₁ ⊔ Subgraph.map f H₂
have verts : ∀ (x : W), x ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
verts : ∀ (x : W), x ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts
⊢ Subgraph.map f (H₁ ⊔ H₂) = Subgraph.map f H₁ ⊔ Subgraph.map f H₂
have Adj : ∀ (x x_1 : W), (Subgraph.map f (H₁ ⊔ H₂)).Adj x x_1 ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ Subgraph.map e.toHom ⊤ = ⊤
have verts : ∀ (x : W), x ∈ (Subgraph.map e.toHom ⊤).verts ↔ Membership.mem (γ := Set W) (verts (G := H) ⊤) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
verts : ∀ (x : W), x ∈ (Subgraph.map e.toHom ⊤).verts ↔ Membership.mem (γ := Set W) (Subgraph.verts (G := H) ⊤) x
⊢ Subgraph.map e.toHom ⊤ = ⊤
have Adj : ∀ (x x_1 : W), (Subgraph.map e.toHom ⊤).Adj x x_1 ↔ Adj (G := H) ⊤ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'
have left : (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
left : (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'
have right : ∀ ⦃v w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
a : V
⊢ a ∈ (Subgraph.comap f H).verts → a ∈ (Subgraph.comap f H').verts
have left : Membership.mem (α := W) H.verts ((f : (a : V) → W) a : W) → Membership.mem (α := W) H'.verts ((f : (a : V) → W) a : W)
Tactic: simp only [comap_verts, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
v w : V
⊢ (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
have right : G.Adj v w → H.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w) → H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)
Tactic: simp +contextual only [comap_adj, and_imp, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
⊢ Subgraph.comap f ⊤ = ⊤
have verts : ∀ (x : V), x ∈ (Subgraph.comap f ⊤).verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊤) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
verts : ∀ (x : V), x ∈ (Subgraph.comap f ⊤).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) ⊤) x
⊢ Subgraph.comap f ⊤ = ⊤
have Adj : ∀ (x x_1 : V), (Subgraph.comap f ⊤).Adj x x_1 ↔ Adj (G := G) ⊤ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
have refine_1 : ∀ (h : Subgraph.map f H ≤ H') (v : V) (hv : v ∈ H.verts), v ∈ (Subgraph.comap f H').verts
Tactic: refine ⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
refine_1 : ∀ (h : Subgraph.map f H ≤ H') (v : V) (hv : v ∈ H.verts), v ∈ (Subgraph.comap f H').verts
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
have refine_2 : ∀ (h : Subgraph.map f H ≤ H') (v w : V) (hvw : H.Adj v w), (Subgraph.comap f H').Adj v w
Tactic: refine ⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
refine_1 : ∀ (h : Subgraph.map f H ≤ H') (v : V) (hv : v ∈ H.verts), v ∈ (Subgraph.comap f H').verts
refine_2 : ∀ (h : Subgraph.map f H ≤ H') (v w : V) (hvw : H.Adj v w), (Subgraph.comap f H').Adj v w
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
have refine_3 : ∀ (h : H ≤ Subgraph.comap f H'), ∀ v ∈ (Subgraph.map f H).verts, v ∈ H'.verts
Tactic: refine ⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
refine_1 : ∀ (h : Subgraph.map f H ≤ H') (v : V) (hv : v ∈ H.verts), v ∈ (Subgraph.comap f H').verts
refine_2 : ∀ (h : Subgraph.map f H ≤ H') (v w : V) (hvw : H.Adj v w), (Subgraph.comap f H').Adj v w
refine_3 : ∀ (h : H ≤ Subgraph.comap f H'), ∀ v ∈ (Subgraph.map f H).verts, v ∈ H'.verts
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
have refine_4 : ∀ (h : H ≤ Subgraph.comap f H') (v w : W), (Subgraph.map f H).Adj v w → H'.Adj v w
Tactic: refine ⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ v ∈ (Subgraph.comap f H').verts
have refine_1 : Membership.mem (α := W) H'.verts ((f : (a : V) → W) v : W)
Tactic: simp only [comap_verts, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ (Subgraph.comap f H').Adj v w
have refine_2 : H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)
Tactic: simp only [H.adj_sub hvw, comap_adj, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts
have refine_3 : ∀ x ∈ H.verts, (f : (a : V) → W) x = v → v ∈ H'.verts
Tactic: simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w
have refine_4 : ∀ (x x_1 : V), H.Adj x x_1 → (f : (a : V) → W) x = v → (f : (a : V) → W) x_1 = w → H'.Adj v w
Tactic: simp only [Relation.Map, map_adj, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ Fintype G.Subgraph
have refine_1 : Function.Injective (β := G.Subgraph)
  fun
    (H :
      { H : Finset V × (V → V → Bool) //
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
  { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
    Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := sorry, edge_vert := sorry, symm := sorry }
Tactic: refine .ofBijective
    (α := {H : Finset V × (V → V → Bool) //
      (∀ a b, H.2 a b → G.Adj a b) ∧ (∀ a b, H.2 a b → a ∈ H.1) ∧ ∀ a b, H.2 a b = H.2 b a})
    (fun H ↦ ⟨H.1.1, fun a b ↦ H.1.2 a b, @H.2.1, @H.2.2.1, by simp [Symmetric, H.2.2.2]⟩)
    ⟨?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
refine_1 :
  Function.Injective (β := G.Subgraph)
    fun
      (H :
        { H : Finset V × (V → V → Bool) //
          (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
            (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
    { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
      Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ Fintype G.Subgraph
have refine_2 : ∀ (H : G.Subgraph),
  ∃ (a :
    { H : Finset V × (V → V → Bool) //
      (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
        (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }),
    (fun
            (H :
              { H : Finset V × (V → V → Bool) //
                (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                  (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
          { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
            Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := sorry, edge_vert := sorry,
            symm := sorry : G.Subgraph })
        a =
      H
Tactic: refine .ofBijective
    (α := {H : Finset V × (V → V → Bool) //
      (∀ a b, H.2 a b → G.Adj a b) ∧ (∀ a b, H.2 a b → a ∈ H.1) ∧ ∀ a b, H.2 a b = H.2 b a})
    (fun H ↦ ⟨H.1.1, fun a b ↦ H.1.2 a b, @H.2.1, @H.2.2.1, by simp [Symmetric, H.2.2.2]⟩)
    ⟨?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst : Finite V
⊢ Finite.{u + 1} G.Subgraph
have intro : ∀ (val : Fintype V), Finite.{u + 1} G.Subgraph
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst : Finite V
⊢ Finite.{u + 1} G.Subgraph
have intro : ∀ (val : Fintype V), Finite.{u + 1} G.Subgraph
Tactic: classical cases nonempty_fintype V; infer_instance
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
G' : G.Subgraph
inst_1 : Fintype (↑G'.verts : Type u)
h : G'.IsSpanning
⊢ G'.verts.toFinset.card = Fintype.card V
have simp : Finset.card.{u} (α := V) Finset.univ = Fintype.card V
Tactic: simp only [isSpanning_iff.1 h, Set.toFinset_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
⊢ (G'.neighborSet v).toFinset.card = G'.degree v
have rw : (G'.neighborSet v).toFinset.card = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
Tactic: rw [degree, Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
rw : (G'.neighborSet v).toFinset.card = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
⊢ (G'.neighborSet v).toFinset.card = G'.degree v
have rw₁ : Fintype.card.{u} (↑(G'.neighborSet v) : Type u) = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
Tactic: rw [degree, Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : v ∉ G'.verts
⊢ G'.degree v = 0
have rw : ∀ (x : V), x ∉ G'.neighborSet v
Tactic: rw [degree, Fintype.card_eq_zero_iff, isEmpty_subtype]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G.neighborSet v) : Type u)
⊢ G'.degree v ≤ G.degree v
have rw : G'.degree v ≤ Fintype.card.{u} (↑(G.neighborSet v) : Type u)
Tactic: rw [← card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : (↑G'.verts : Type u)
inst : Fintype (↑(G'.coe.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.neighborSet (↑v : V)) : Type u)
⊢ G'.coe.degree v = G'.degree (↑v : V)
have rw : Fintype.card.{u} (↑(G'.coe.neighborSet v) : Type u) = G'.degree (↑v : V)
Tactic: rw [← card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
inst_1 : Fintype (↑(G'.spanningCoe.neighborSet v) : Type u)
⊢ G'.spanningCoe.degree v = G'.degree v
have rw : Fintype.card.{u} (↑(G'.spanningCoe.neighborSet v) : Type u) = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
Tactic: rw [← card_neighborSet_eq_degree, Subgraph.degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
⊢ G'.degree v = 0
have pos : ∀ (hv : v ∈ G'.verts), G'.degree v = 0
Tactic: by_cases hv : v ∈ G'.verts
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
pos : ∀ (hv : v ∈ G'.verts), G'.degree v = 0
⊢ G'.degree v = 0
have neg : ∀ (hv : v ∉ G'.verts), G'.degree v = 0
Tactic: by_cases hv : v ∈ G'.verts
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.degree v = 0
have pos : G'.coe.degree (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) = 0
Tactic: rw [← G'.coe_degree ⟨v, hv⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.coe.degree (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) = 0
have this : Subsingleton.{u + 1} (↑G'.verts : Type u)
Tactic: have := (Set.subsingleton_coe _).mpr hG
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
⊢ G'.degree v = 1 ↔ ∃! w : V, G'.Adj v w
have rw : (∃! a : V, a ∈ (G'.neighborSet v).toFinset) ↔ ∃! w : V, G'.Adj v w
Tactic: rw [← finset_card_neighborSet_eq_degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : G'.degree v ≠ 0
⊢ Nontrivial.{u} (↑G'.verts : Type u)
have by_contra : ∀ (this : ¬Nontrivial.{u} (↑G'.verts : Type u)), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : (↑(G.neighborSet v) : Type u) ≃ (↑(H.neighborSet v) : Type u)
hfin : (G.neighborSet v).Finite
⊢ H.neighborSet v = G.neighborSet v
have lift : ∀ (s : Finset V) (hs : (↑s : Set V) = H.neighborSet v) (h : (↑(G.neighborSet v) : Type u) ≃ (↑(↑s : Set V) : Type u)),
  (↑s : Set V) = G.neighborSet v
Tactic: lift H.neighborSet v to Finset V using h.set_finite_iff.mp hfin with s hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
h : (↑(G.neighborSet v) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ (↑s : Set V) = G.neighborSet v
have lift : ∀ (t : Finset V) (ht : (↑t : Set V) = G.neighborSet v) (h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)),
  (↑s : Set V) = (↑t : Set V)
Tactic: lift G.neighborSet v to Finset V using hfin with t ht
Cleared hypotheses: hfin, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ (↑s : Set V) = (↑t : Set V)
have refine : s ⊆ t
Tactic: refine congrArg _ <| Finset.eq_of_subset_of_card_le ?_ (Finset.card_eq_of_equiv h).le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : (↑s : Set V) = H.neighborSet v
t : Finset V
ht : (↑t : Set V) = G.neighborSet v
h : (↑(↑t : Set V) : Type u) ≃ (↑(↑s : Set V) : Type u)
⊢ s ⊆ t
have rw : H.neighborSet v ⊆ G.neighborSet v
Tactic: rw [← Finset.coe_subset, hs, ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
⊢ Fintype.card.{u} (↑((toSubgraph H h).neighborSet v) : Type u) = H.degree v
have refine : ↥(H.neighborFinset v) ≃ (↑((toSubgraph H h).neighborSet v) : Type u)
Tactic: refine (Finset.card_eq_of_equiv_fintype ?_).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst : Fintype (↑((toSubgraph H h).neighborSet v) : Type u)
inst_1 : Fintype (↑(H.neighborSet v) : Type u)
⊢ ↥(H.neighborFinset v) ≃ (↑((toSubgraph H h).neighborSet v) : Type u)
have simp : { x : V // H.Adj v x } ≃ { x : V // H.Adj v x }
Tactic: simp only [mem_neighborFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts
have refine : v ∈ H.verts → G.singletonSubgraph v ≤ H
Tactic: refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ G.singletonSubgraph v ≤ H
have left : (G.singletonSubgraph v).verts ⊆ H.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
left : (G.singletonSubgraph v).verts ⊆ H.verts
⊢ G.singletonSubgraph v ≤ H
have right : ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w
Tactic: constructor