awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
⊢ E(G) = ∅
have rw : E(noEdge V(G) β) = ∅
Tactic: rw [h, edgeSet_noEdge]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
rw : E(noEdge V(G) β) = ∅
⊢ E(G) = ∅
have rw₁ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [h, edgeSet_noEdge]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ E(G) = ∅ ↔ G = noEdge V(G) β
have refine : ∀ (h : E(G) = ∅) (e : β) (x y : α), G.IsLink e x y ↔ (noEdge V(G) β).IsLink e x y
Tactic: refine ⟨fun h ↦ Graph.ext rfl ?_, fun h ↦ by rw [h, edgeSet_noEdge]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
⊢ ∀ (e : β) (x y : α), G.IsLink e x y ↔ (noEdge V(G) β).IsLink e x y
have simp : ∀ (e : β) (x y : α), ¬G.IsLink e x y
Tactic: simp only [noEdge_isLink, iff_false]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ False
have this : Membership.mem (γ := Set β) ∅ e
Tactic: have := h ▸ he.edge_mem
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)
have simp : e ∈ edgeSet → ((∃ (x_1 : α), x = u ∧ x_1 = v ∨ x = v ∧ x_1 = u) ↔ x = u ∨ x = v)
Tactic: simp only [Inc, banana_isLink, exists_and_left, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v
have simp_rw : (e ∈ edgeSet ∧ (x = u ∨ x = v)) ∧ ¬(e ∈ edgeSet ∧ (x = u ∧ x = v ∨ x = v ∧ x = u)) ↔
  e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v
Tactic: simp_rw [isNonloopAt_iff_inc_not_isLoopAt, ← isLink_self_iff, banana_isLink, banana_inc]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = u ∧ u = v
have simp : e ∈ edgeSet → (x = u ∧ x = v ∨ x = v ∧ x = u ↔ x = u ∧ u = v)
Tactic: simp only [← isLink_self_iff, banana_isLink, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
⊢ (banana u v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ s(x, y) = s(u, v)
have simp : x = u ∧ y = v ∨ x = v ∧ y = u → ((∃ (x : β), x ∈ edgeSet) ↔ edgeSet.Nonempty)
Tactic: simp only [Adj, banana_isLink, exists_and_right, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
u v : α
⊢ banana u v ∅ = noEdge {u, v} β
have hV : ∀ (x : α), x ∈ vertexSet.{u_1, u_2} (β := β) (banana u v ∅) ↔ Membership.mem (γ := Set α) V(noEdge {u, v} β) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
u v : α
hV : ∀ (x : α), x ∈ vertexSet.{u_1, u_2} (β := β) (banana u v ∅) ↔ Membership.mem (γ := Set α) V(noEdge {u, v} β) x
⊢ banana u v ∅ = noEdge {u, v} β
have h : ∀ (e : β) (x y : α), IsLink (banana u v ∅) e x y ↔ IsLink (noEdge {u, v} β) e x y
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
⊢ G = bouquet v E(G)
have hrw : V(G) = {v}
Tactic: have hrw := hss.eq_singleton_of_mem hv
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
⊢ G = bouquet v E(G)
have refine_1 : ∀ (e : β) (x : α) (h : G.Inc e x), (bouquet v E(G)).Inc e x
Tactic: refine Graph.ext_inc (by simpa) fun e x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
refine_1 : ∀ (e : β) (x : α) (h : G.Inc e x), (bouquet v E(G)).Inc e x
⊢ G = bouquet v E(G)
have refine_2 : ∀ (e : β) (x : α) (h : (bouquet v E(G)).Inc e x), G.Inc e x
Tactic: refine Graph.ext_inc (by simpa) fun e x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : (bouquet v E(G)).Inc e x
⊢ G.Inc e x
have h₁ : e ∈ E(G) ∧ x = v
Tactic: simp only [bouquet_inc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
⊢ G.Inc e x
have refine_2 : ∀ (z w : α) (hzw : G.IsLink e z w), G.Inc e x
Tactic: obtain ⟨z, w, hzw⟩ := exists_isLink_of_mem_edgeSet h.1
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
v : α
G : Graph α β
hv : v ∈ V(G)
hss : V(G).Subsingleton
hrw : V(G) = {v}
e : β
x : α
h : e ∈ E(G) ∧ x = v
z w : α
hzw : G.IsLink e z w
⊢ G.Inc e x
have refine_2 : G.Inc e z
Tactic: rw [h.2, ← show z = v from (show z ∈ {v} from hrw ▸ hzw.left_mem)]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
⊢ G.restrict (F ∩ E(G)) = G.restrict F
have rw : G.restrict (E(G) ∩ F) = G.restrict F
Tactic: rw [inter_comm, restrict_edgeSet_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F : Set β
rw : G.restrict (E(G) ∩ F) = G.restrict F
⊢ G.restrict (F ∩ E(G)) = G.restrict F
have rw₁ : G.restrict F = G.restrict F
Tactic: rw [inter_comm, restrict_edgeSet_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.restrict F ≤ G.restrict F
have refine_1 : V(H.restrict F) ⊆ V(G.restrict F)
Tactic: refine (Compatible.of_le_le (G := G) (restrict_le.trans h) (by simp)).le_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
refine_1 : V(H.restrict F) ⊆ V(G.restrict F)
⊢ H.restrict F ≤ G.restrict F
have refine_2 : E(H.restrict F) ⊆ E(G.restrict F)
Tactic: refine (Compatible.of_le_le (G := G) (restrict_le.trans h) (by simp)).le_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)
have refine : E((G.restrict F₁).restrict F₂) = E(G.restrict (F₁ ∩ F₂))
Tactic: refine (Compatible.of_le_le (G := G) (restrict_le.trans (by simp)) (by simp)).ext (by simp) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ E(G) ∩ F₁ ∩ F₂ = E(G) ∩ (F₁ ∩ F₂)
have rw : E(G) ∩ F₁ ∩ F₂ = E(G) ∩ F₁ ∩ F₂
Tactic: rw [← inter_assoc, inter_comm _ F₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : E(G) ∩ F₁ ∩ F₂ = E(G) ∩ F₁ ∩ F₂
⊢ E(G) ∩ F₁ ∩ F₂ = E(G) ∩ (F₁ ∩ F₂)
have rw₁ : F₂ ∩ (E(G) ∩ F₁) = F₂ ∩ (E(G) ∩ F₁)
Tactic: rw [← inter_assoc, inter_comm _ F₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H : Graph α β
F_1 F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ (G.restrict (E(G) \ F)).IsLink e x y ↔ (fun (e : β) (x y : α) ↦ G.IsLink e x y ∧ e ∉ F) e x y
have simp : G.IsLink e x y → e ∉ F → e ∈ E(G)
Tactic: simp only [restrict_isLink, mem_diff, and_comm, and_congr_left_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.deleteEdges F ≤ G.deleteEdges F
have simp_rw : H.restrict (E(H) \ F) ≤ G.restrict (E(G) \ F)
Tactic: simp_rw [← restrict_edgeSet_diff_eq_deleteEdges]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.restrict (E(H) \ F) ≤ G.restrict (E(G) \ F)
have refine : E(H) \ F ⊆ E(G) \ F
Tactic: refine (restrict_mono_left h (E(H) \ F)).trans (G.restrict_mono_right ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G : Graph α β
F : Set β
⊢ (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F
have simp : G.IsLoopAt e x → e ∉ F → e ∈ E(G)
Tactic: simp only [← restrict_edgeSet_diff_eq_deleteEdges, restrict_isLoopAt, mem_diff,
    and_congr_right_iff, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)
have simp : G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
Tactic: simp only [← restrict_edgeSet_diff_eq_deleteEdges, diff_eq_compl_inter, restrict_inter_edgeSet,
    edgeSet_restrict, restrict_restrict, compl_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₆ : G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₆ : G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₇ : G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₆ : G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₇ : G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₈ : G.restrict (F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
rw : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
rw₁ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₂ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₃ : G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₄ : G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₅ : G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₆ : G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₇ : G.restrict (F₁ᶜ ∩ F₂ᶜ ∩ E(G)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
rw₈ : G.restrict (F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
⊢ G.restrict (F₁ᶜ ∩ (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ))) = G.restrict (F₁ᶜ ∩ F₂ᶜ)
have rw₉ : G.restrict (F₂ᶜ ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Tactic: rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.induce V(G) = G
have refine : ∀ (e : β) (h : e ∈ E(G)), e ∈ E(G.induce V(G))
Tactic: refine (Compatible.of_le_le (G := G) (by simp) (by simp)).ext rfl <| Set.ext fun e ↦
    ⟨fun ⟨_, _, h⟩ ↦ h.1.edge_mem, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
e : β
h : e ∈ E(G)
⊢ e ∈ E(G.induce V(G))
have obtain : ∀ (x y : α) (h : G.IsLink e x y), e ∈ E(G.induce V(G))
Tactic: obtain ⟨x, y, h⟩ := exists_isLink_of_mem_edgeSet h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Delete (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
X : Set α
⊢ (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X
have simp : G.IsLink e x y → ((x ∈ V(G) ∧ x ∉ X) ∧ y ∈ V(G) ∧ y ∉ X ↔ x ∉ X ∧ y ∉ X)
Tactic: simp only [deleteVerts, induce_isLink, mem_diff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
x y : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
⊢ Membership.mem (γ := Set β) {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} e ↔
    ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y
have simp : (((∃ (x : α) (y : α), G.IsLink e x y) ∧ ∃ (x : α) (y : α), H.IsLink e x y) ∧
    ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y) ↔
  ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y
Tactic: simp only [edgeSet_eq_setOf_exists_isLink, mem_inter_iff, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
h : ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y
x y : α
hfG : G.IsLink e x y
hfH : H.IsLink e x y
z w : α
⊢ G.IsLink e z w ↔ H.IsLink e z w
have rw : s(x, y) = s(z, w) ↔ H.IsLink e z w
Tactic: rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
h : ∃ (x : α) (y : α), G.IsLink e x y ∧ H.IsLink e x y
x y : α
hfG : G.IsLink e x y
hfH : H.IsLink e x y
z w : α
rw : s(x, y) = s(z, w) ↔ H.IsLink e z w
⊢ G.IsLink e z w ↔ H.IsLink e z w
have rw₁ : s(x, y) = s(z, w) ↔ s(x, y) = s(z, w)
Tactic: rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ Disjoint G H ↔ Disjoint V(G) V(H)
have rw : G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)
Tactic: rw [disjoint_iff, ← vertexSet_eq_empty_iff, vertexSet_inf, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
rw : G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)
⊢ Disjoint G H ↔ Disjoint V(G) V(H)
have rw₁ : V(G ⊓ H) = ∅ ↔ Disjoint V(G) V(H)
Tactic: rw [disjoint_iff, ← vertexSet_eq_empty_iff, vertexSet_inf, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
rw : G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)
rw₁ : V(G ⊓ H) = ∅ ↔ Disjoint V(G) V(H)
⊢ Disjoint G H ↔ Disjoint V(G) V(H)
have rw₂ : V(G) ∩ V(H) = ∅ ↔ Disjoint V(G) V(H)
Tactic: rw [disjoint_iff, ← vertexSet_eq_empty_iff, vertexSet_inf, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
rw : G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)
rw₁ : V(G ⊓ H) = ∅ ↔ Disjoint V(G) V(H)
rw₂ : V(G) ∩ V(H) = ∅ ↔ Disjoint V(G) V(H)
⊢ Disjoint G H ↔ Disjoint V(G) V(H)
have rw₃ : V(G) ∩ V(H) = ∅ ↔ V(G) ∩ V(H) = ∅
Tactic: rw [disjoint_iff, ← vertexSet_eq_empty_iff, vertexSet_inf, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G_1 H : Graph α β
f_1 g : α → α'
u v : α
e_1 : β
x_1 y_1 : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z w : α
hzw : G.IsLink e z w
⊢ f x = f z ∨ f x = f w
have inl : ∀ (hzw : G.IsLink e x w), f x = f x ∨ f x = f w
Tactic: obtain rfl | rfl := hxy.left_eq_or_eq hzw
Cleared hypotheses: z, hzw
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G_1 H : Graph α β
f_1 g : α → α'
u v : α
e_1 : β
x_1 y_1 : α'
f : α → α'
G : Graph α β
e : β
x y : α
hxy : G.IsLink e x y
z w : α
hzw : G.IsLink e z w
inl : ∀ (hzw : G.IsLink e x w), f x = f x ∨ f x = f w
⊢ f x = f z ∨ f x = f w
have inr : ∀ (hzw : G.IsLink e z x), f x = f z ∨ f x = f x
Tactic: obtain rfl | rfl := hxy.left_eq_or_eq hzw
Cleared hypotheses: w, hzw
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G_1 H : Graph α β
f_1 g : α → α'
u v : α
e_1 : β
x y : α'
f : α → α'
G : Graph α β
e : β
⊢ e ∈ E(G) ↔ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
have refine : ∀ (h : e ∈ E(G)), ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
Tactic: refine ⟨fun h ↦ ?_, fun ⟨_, _, _, _, h, _, _⟩ ↦ h.edge_mem⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G_1 H : Graph α β
f_1 g : α → α'
u v : α
e_1 : β
x y : α'
f : α → α'
G : Graph α β
e : β
h : e ∈ E(G)
⊢ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
have obtain : ∀ (x y : α) (hxy : G.IsLink e x y), ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
Tactic: obtain ⟨x, y, hxy⟩ := exists_isLink_of_mem_edgeSet h
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mpr : (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
mp : (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
mpr :
  (∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v) → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
⊢ (∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔ ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
have mp₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → ∃ (v : α), (∃ (y : α), G.IsLink e v y) ∧ x = f v
Tactic: tauto