awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
hs : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') ∈ s →
    ¬Sym2.Rel V (v', w') (v, w)
have Adj : Sym2.Rel V (v', w') (v, w) →
  s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') ∉ s
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' s)
have Adj : ∀ (v : V) (hv : v ∈ (G'.deleteEdges s).verts) (w : V) (hw : w ∈ (G'.deleteEdges s).verts),
  (G'.deleteEdges s).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteEdges s).verts) v hv)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteEdges s).verts) w hw) ↔
    (G'.coe.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) ⁻¹' s)).Adj
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteEdges s).verts) v hv)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G'.deleteEdges s).verts) w hw)
Tactic: ext ⟨v, hv⟩ ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges s ≤ G'
have left : (G'.deleteEdges s).verts ⊆ G'.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
left : (G'.deleteEdges s).verts ⊆ G'.verts
⊢ G'.deleteEdges s ≤ G'
have right : ∀ ⦃v w : V⦄, (G'.deleteEdges s).Adj v w → G'.Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ G'.deleteEdges s' ≤ G'.deleteEdges s
have left : (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
left : (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts
⊢ G'.deleteEdges s' ≤ G'.deleteEdges s
have right : ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w
have right : ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s
Tactic: simp +contextual only [deleteEdges_verts, deleteEdges_adj,
    true_and, and_imp, subset_rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s
have verts : ∀ (x : V), x ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x ∈ (G'.deleteEdges s).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
verts : ∀ (x : V), x ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x ∈ (G'.deleteEdges s).verts
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s
have Adj : ∀ (x x_1 : V), (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x x_1 ↔ (G'.deleteEdges s).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s
have verts : ∀ (x : V), x ∈ (G'.deleteEdges (s ∩ G'.edgeSet)).verts ↔ x ∈ (G'.deleteEdges s).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
verts : ∀ (x : V), x ∈ (G'.deleteEdges (s ∩ G'.edgeSet)).verts ↔ x ∈ (G'.deleteEdges s).verts
⊢ G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s
have Adj : ∀ (x x_1 : V), (G'.deleteEdges (s ∩ G'.edgeSet)).Adj x x_1 ↔ (G'.deleteEdges s).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ SimpleGraph.induce s G = Subgraph.coe (induce ⊤ s)
have Adj : ∀ (x x_1 : (↑s : Type u)), (SimpleGraph.induce s G).Adj x x_1 ↔ SimpleGraph.Adj (Subgraph.coe (induce ⊤ s)) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ Subgraph.spanningCoe (G := G) (induce ⊤ s) = (SimpleGraph.induce s G).spanningCoe (s := s)
have rw : Subgraph.spanningCoe (G := G) (induce ⊤ s) =
  spanningCoe (s := s) (Subgraph.coe (induce ⊤ s) : SimpleGraph (↑(verts (G := G) (induce ⊤ s)) : Type u))
Tactic: rw [induce_eq_coe_induce_top]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.IsInduced ↔ ∃ (s : Set V), G' = induce ⊤ s
have refine : (∃ (s : Set V), G' = induce ⊤ s) →
  ∀ (x : V) (hu : x ∈ G'.verts) (x_1 : V) (hv : x_1 ∈ G'.verts) (hadj : G.Adj x x_1) (s : Set V) (h : G' = induce ⊤ s),
    G'.Adj x x_1
Tactic: refine ⟨fun h ↦ ⟨G'.verts, h.induce_top_verts.symm⟩, fun ⟨s, h⟩ _ hu _ hv hadj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : ∃ (s : Set V), G' = induce ⊤ s
x : V
hu : x ∈ G'.verts
x_1 : V
hv : x_1 ∈ G'.verts
hadj : G.Adj x x_1
s : Set V
h : G' = induce ⊤ s
⊢ G'.Adj x x_1
have rw : Adj (G := G) (induce ⊤ G'.verts) x x_1
Tactic: rw [h, (h ▸ rfl : s = G'.verts)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ G'.induce s ≤ G''.induce s'
have left : (G'.induce s).verts ⊆ (G''.induce s').verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
left : (G'.induce s).verts ⊆ (G''.induce s').verts
⊢ G'.induce s ≤ G''.induce s'
have right : ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w
have right : ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
Tactic: simp +contextual only [induce_adj, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce ∅ = ⊥
have verts : ∀ (x : V), x ∈ (G'.induce ∅).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
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.induce ∅).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) ⊥) x
⊢ G'.induce ∅ = ⊥
have Adj : ∀ (x x_1 : V), (G'.induce ∅).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
G' : G.Subgraph
⊢ G'.induce G'.verts = G'
have verts : ∀ (x : V), x ∈ (G'.induce G'.verts).verts ↔ x ∈ G'.verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.induce G'.verts).verts ↔ x ∈ G'.verts
⊢ G'.induce G'.verts = G'
have Adj : ∀ (x x_1 : V), (G'.induce G'.verts).Adj x x_1 ↔ G'.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ (G'.induce G'.verts).Adj x x_1 ↔ G'.Adj x x_1
have Adj : (G'.induce G'.verts).Adj x x_1 → G'.Adj x x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
Adj : (G'.induce G'.verts).Adj x x_1 → G'.Adj x x_1
⊢ (G'.induce G'.verts).Adj x x_1 ↔ G'.Adj x x_1
have Adj₁ : G'.Adj x x_1 → (G'.induce G'.verts).Adj x x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x x_1 : V
⊢ G'.Adj x x_1 → (G'.induce G'.verts).Adj x x_1
have Adj : G'.Adj x x_1 → x ∈ G'.verts ∧ x_1 ∈ G'.verts
Tactic: simp +contextual only [induce_adj, imp_true_iff, and_true]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')
have left : (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
left : (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')
have right : ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ G.singletonSubgraph v = induce ⊤ {v}
have verts : ∀ (x : V), x ∈ (G.singletonSubgraph v).verts ↔ Membership.mem (γ := Set V) (verts (G := G) (induce ⊤ {v})) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
verts :
  ∀ (x : V), x ∈ (G.singletonSubgraph v).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) (induce ⊤ {v})) x
⊢ G.singletonSubgraph v = induce ⊤ {v}
have Adj : ∀ (x x_1 : V), (G.singletonSubgraph v).Adj x x_1 ↔ Adj (G := G) (induce ⊤ {v}) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj hvw = induce ⊤ {v, w}
have verts : ∀ (x : V), x ∈ (G.subgraphOfAdj hvw).verts ↔ Membership.mem (γ := Set V) (verts (G := G) (induce ⊤ {v, w})) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
verts :
  ∀ (x : V), x ∈ (G.subgraphOfAdj hvw).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) (induce ⊤ {v, w})) x
⊢ G.subgraphOfAdj hvw = induce ⊤ {v, w}
have Adj : ∀ (x x_1 : V), (G.subgraphOfAdj hvw).Adj x x_1 ↔ Adj (G := G) (induce ⊤ {v, w}) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
⊢ (G.subgraphOfAdj hvw).Adj x x_1 ↔ Adj (G := G) (induce ⊤ {v, w}) x x_1
have Adj : (G.subgraphOfAdj hvw).Adj x x_1 → Adj (G := G) (induce ⊤ {v, w}) x x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
Adj : (G.subgraphOfAdj hvw).Adj x x_1 → Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1 ↔ Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1
have Adj₁ : Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1 → (G.subgraphOfAdj hvw).Adj x x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (G.subgraphOfAdj hvw).Adj x x_1
⊢ Adj (G := G) (induce ⊤ {v, w}) x x_1
have h₁ : v = x ∧ w = x_1 ∨ v = x_1 ∧ w = x
Tactic: simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : v = x ∧ w = x_1 ∨ v = x_1 ∧ w = x
⊢ Adj (G := G) (induce ⊤ {v, w}) x x_1
have Adj : Adj (G := G) (induce ⊤ {v, w}) v w
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h
Cleared hypotheses: x, x_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : v = x ∧ w = x_1 ∨ v = x_1 ∧ w = x
Adj : Subgraph.Adj (G := G) (induce ⊤ {v, w}) v w
⊢ Subgraph.Adj (G := G) (induce ⊤ {v, w}) x x_1
have Adj₁ : Subgraph.Adj (G := G) (induce ⊤ {v, w}) w v
Tactic: obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h
Cleared hypotheses: x, x_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : Adj (G := G) (induce ⊤ {v, w}) x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1
have h₁ : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
Tactic: simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1
have Adj : ∀ (hvw : G.Adj x_1 w) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
Tactic: obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h
Cleared hypotheses: v, hvw, x, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
Adj : ∀ (hvw : G.Adj x_1 w) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1
have Adj₁ : ∀ (ha hvw : G.Adj x x_1), (G.subgraphOfAdj hvw).Adj x x_1
Tactic: obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h
Cleared hypotheses: v, w, hvw, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
Adj : ∀ (hvw : G.Adj x_1 w) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
Adj₁ : ∀ (ha hvw : G.Adj x x_1), (G.subgraphOfAdj hvw).Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1
have Adj₂ : ∀ (ha : G.Adj x x_1) (hvw : G.Adj x_1 x), (G.subgraphOfAdj hvw).Adj x x_1
Tactic: obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h
Cleared hypotheses: v, w, hvw, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x x_1 : V
h : (x = v ∨ x = w) ∧ (x_1 = v ∨ x_1 = w) ∧ G.Adj x x_1
Adj : ∀ (hvw : G.Adj x_1 w) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
Adj₁ : ∀ (ha hvw : G.Adj x x_1), (G.subgraphOfAdj hvw).Adj x x_1
Adj₂ : ∀ (ha : G.Adj x x_1) (hvw : G.Adj x_1 x), (G.subgraphOfAdj hvw).Adj x x_1
⊢ (G.subgraphOfAdj hvw).Adj x x_1
have Adj₃ : ∀ (hvw : G.Adj v x_1) (ha : G.Adj x_1 x_1), (G.subgraphOfAdj hvw).Adj x_1 x_1
Tactic: obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h
Cleared hypotheses: w, hvw, x, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')
have verts : ∀ (x : V), x ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x ∈ (G'.deleteVerts (s ∪ s')).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
verts : ∀ (x : V), x ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x ∈ (G'.deleteVerts (s ∪ s')).verts
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')
have Adj : ∀ (x x_1 : V), ((G'.deleteVerts s).deleteVerts s').Adj x x_1 ↔ (G'.deleteVerts (s ∪ s')).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts s ≤ G'
have left : (G'.deleteVerts s).verts ⊆ G'.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
left : (G'.deleteVerts s).verts ⊆ G'.verts
⊢ G'.deleteVerts s ≤ G'
have right : ∀ ⦃v w : V⦄, (G'.deleteVerts s).Adj v w → G'.Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s
have verts : ∀ (x : V), x ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x ∈ (G'.deleteVerts s).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
verts : ∀ (x : V), x ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x ∈ (G'.deleteVerts s).verts
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s
have Adj : ∀ (x x_1 : V), (G'.deleteVerts (G'.verts ∩ s)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s
have verts : ∀ (x : V), x ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x ∈ (G'.deleteVerts s).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
verts : ∀ (x : V), x ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x ∈ (G'.deleteVerts s).verts
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s
have Adj : ∀ (x x_1 : V), (G'.deleteVerts (s ∩ G'.verts)).Adj x x_1 ↔ (G'.deleteVerts s).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G_1 : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
G : SimpleGraph V
H : SimpleGraph W
u : V ⊕ W
⊢ ¬match (motive := V ⊕ W → V ⊕ W → Prop) u, u with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true
have inl : ∀ (val : V),
  ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inl val, Sum.inl val with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G_1 : SimpleGraph V
H_1 : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
G : SimpleGraph V
H : SimpleGraph W
u : V ⊕ W
inl :
  ∀ (val : V),
    ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inl val, Sum.inl val with
      | Sum.inl u, Sum.inl v => G.Adj u v
      | Sum.inr u, Sum.inr v => H.Adj u v
      | x, x_1 => false = true
⊢ ¬match (motive := V ⊕ W → V ⊕ W → Prop) u, u with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true
have inr : ∀ (val : W),
  ¬match (motive := V ⊕ W → V ⊕ W → Prop) Sum.inr val, Sum.inr val with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_1 => false = true
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
f : G →g G'
g : H →g H'
u v : V ⊕ W
⊢ (G ⊕g H).Adj u v →
    (G' ⊕g H').Adj (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') u)
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
have inl : ∀ (val : V),
  (G ⊕g H).Adj (Sum.inl val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
f : G →g G'
g : H →g H'
u v : V ⊕ W
inl :
  ∀ (val : V),
    (G ⊕g H).Adj (Sum.inl val) v →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
⊢ (G ⊕g H).Adj u v →
    (G' ⊕g H').Adj (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') u)
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
have inr : ∀ (val : W),
  (G ⊕g H).Adj (Sum.inr val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
Tactic: cases u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val : V
⊢ (G ⊕g H).Adj (Sum.inl val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
have inl : ∀ (val_1 : V),
  (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v_1 v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val : V
inl :
  ∀ (val_1 : V),
    (G ⊕g H).Adj (Sum.inl val) (Sum.inl val_1) →
      (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
        (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val_1))
⊢ (G ⊕g H).Adj (Sum.inl val) v →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map (⇑f : (a : V) → V') (⇑g : (a : W) → W') v)
have inl₁ : ∀ (val_1 : W),
  (G ⊕g H).Adj (Sum.inl val) (Sum.inr val_1) →
    (G' ⊕g H').Adj (Sum.map.{u_3, u_4, u_5, u_6} (β := W) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inl val))
      (Sum.map.{u_3, u_4, u_5, u_6} (α := V) (⇑f : (a : V) → V') (⇑g : (a : W) → W') (Sum.inr val_1))
Tactic: cases v
Cleared hypotheses: v