awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Graph.Lattice
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
rw₁ rw₂ : s(x, y) = s(z, w) ↔ s(x, y) = s(z, w)
⊢ G.IsLink e z w ↔ H.IsLink e z w

Tactic:
rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]

Premises used: Graph.IsLink.isLink_iff_sym2_eq
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x y : α
e_1 : β
G_1 H_1 G H : Graph α β
e : β
⊢ (((∃ (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:
exact ⟨fun ⟨⟨⟨x, y, hexy⟩, ⟨z, w, hezw⟩⟩, h⟩ ↦ ⟨x, y, hexy, by rwa [← h]⟩,
        fun ⟨x, y, hfG, hfH⟩ ↦ ⟨⟨⟨_, _, hfG⟩, ⟨_, _, hfH⟩⟩,
        fun z w ↦ by rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]⟩⟩
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G_1 H_1 G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    IsLink
        { vertexSet := V(G) ∩ V(H), IsLink := fun (e : β) (x y : α) ↦ G.IsLink e x y ∧ H.IsLink e x y,
          edgeSet := {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
          eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
        e x y →
      G.IsLink e x y

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G_1 H_1 G H : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄,
    IsLink
        { vertexSet := V(G) ∩ V(H), IsLink := fun (e : β) (x y : α) ↦ G.IsLink e x y ∧ H.IsLink e x y,
          edgeSet := {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}, isLink_symm := ⋯,
          eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
        e x y →
      H.IsLink e x y

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 : α
e_1 : β
G H_1 H G₁ G₂ : Graph α β
h₁ : H ≤ G₁
h₂ : H ≤ G₂
e : β
x y : α
h : H.IsLink e x y
⊢ IsLink
    { vertexSet := V(G₁) ∩ V(G₂), IsLink := fun (e : β) (x y : α) ↦ G₁.IsLink e x y ∧ G₂.IsLink e x y,
      edgeSet := {e : β | e ∈ E(G₁) ∩ E(G₂) ∧ ∀ (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y}, isLink_symm := ⋯,
      eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
    e x y

Tactic:
simp [h₁.isLink_mono h, h₂.isLink_mono h]

Premises used: Graph.IsSubgraph.isLink_mono
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ V(G ⊓ H) = V(G) ∩ V(H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ E(G ⊓ H) = {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).Inc e x ↔ ∃ (y : α), G.IsLink e x y ∧ H.IsLink e x y

Tactic:
simp [Inc]

Premises used: Graph.Inc
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsLoopAt e x ↔ G.IsLoopAt e x ∧ H.IsLoopAt e x

Tactic:
simp [← isLink_self_iff]

Premises used: Graph.isLink_self_iff
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
⊢ (G ⊓ H).IsNonloopAt e x ↔ ∃ (y : α), y ≠ x ∧ G.IsLink e x y ∧ H.IsLink e x y

Tactic:
simp [IsNonloopAt]

Premises used: Graph.IsNonloopAt
-- Module: Mathlib.Combinatorics.Graph.Lattice
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)
rw₃ rw₄ : V(G) ∩ V(H) = ∅ ↔ V(G) ∩ V(H) = ∅
⊢ Disjoint G H ↔ Disjoint V(G) V(H)

Tactic:
rw [disjoint_iff, ← vertexSet_eq_empty_iff, vertexSet_inf, disjoint_iff_inter_eq_empty]

Premises used: Graph.vertexSet_eq_empty_iff, Graph.vertexSet_inf, disjoint_iff, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} = E(G) ∩ E(H)

Tactic:
le_antisymm (fun e he ↦ he.1) fun e he ↦ ⟨he, fun _ _ ↦ h.isLink_congr he.1 he.2⟩

Premises used: Graph.Compatible.isLink_congr, le_antisymm, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Graph.Lattice
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ {e : β | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} = E(G) ∩ E(H)

Tactic:
exact le_antisymm (fun e he ↦ he.1) fun e he ↦ ⟨he, fun _ _ ↦ h.isLink_congr he.1 he.2⟩

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.Graph.Maps
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
inr : ∀ (hzw : G.IsLink e z x), f x = f z ∨ f x = f x
⊢ f x = f z ∨ f x = f w

Tactic:
obtain rfl | rfl := hxy.left_eq_or_eq hzw

Premises used: Graph.IsLink.left_eq_or_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Maps
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
w : α
hzw : G.IsLink e x w
⊢ f x = f x ∨ f x = f w

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : α
hzw : G.IsLink e z x
⊢ f x = f z ∨ f x = f x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Maps
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

Tactic:
⟨fun h ↦ ?_, fun ⟨_, _, _, _, h, _, _⟩ ↦ h.edge_mem⟩

Premises used: Graph.IsLink.edge_mem, Membership.mem, Iff.intro, Graph.edgeSet, _private.0.Graph.map.match_1
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : β
refine : ∀ (h : e ∈ E(G)), ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
⊢ e ∈ E(G) ↔ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨_, _, _, _, h, _, _⟩ ↦ h.edge_mem⟩
-- Module: Mathlib.Combinatorics.Graph.Maps
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)
obtain : ∀ (x y : α) (hxy : G.IsLink e x y), ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y
⊢ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y

Tactic:
obtain ⟨x, y, hxy⟩ := exists_isLink_of_mem_edgeSet h

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : β
h : e ∈ E(G)
x y : α
hxy : G.IsLink e x y
⊢ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y

Tactic:
⟨_, _, _, _, hxy, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : β
h : e ∈ E(G)
x y : α
hxy : G.IsLink e x y
⊢ ∃ (x : α') (y : α'), Relation.Map (G.IsLink e) f f x y

Tactic:
exact ⟨_, _, _, _, hxy, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : α
h : G.IsLink e x y
⊢ f x ∈ f '' V(G)

Tactic:
Set.mem_image_of_mem _ h.left_mem

Premises used: Graph.IsLink.left_mem, Set.mem_image_of_mem
-- Module: Mathlib.Combinatorics.Graph.Maps
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 : α
h : G.IsLink e x y
⊢ f x ∈ f '' V(G)

Tactic:
exact Set.mem_image_of_mem _ h.left_mem

Premises used: Graph.IsLink.left_mem, Set.mem_image_of_mem
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
e : β
f : α → α'
h : G.IsLink e u v
⊢ (map f G).IsLink e (f u) (f v)

Tactic:
⟨u, v, h, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl, Relation.Map
-- Module: Mathlib.Combinatorics.Graph.Maps
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
mp₁ mp₂ 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
mpr₁ mpr₂ mpr₃ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ 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
mpr₄ mpr₅ mpr₆ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ 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
mp₉ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₀ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mp₁₁ : ∀ (w : α') (w_1 w_2 : α), G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → (∃ (y : α), G.IsLink e w_1 y) ∧ x = f w_1
mp₁₂ : (w : α') → (w_1 w_2 : α) → G.IsLink e w_1 w_2 → f w_1 = x → f w_2 = w → α
mpr₇ mpr₈ :
  ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (y : α') (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mpr₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₀ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₁ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = f w_1
mpr₁₂ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₃ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
mpr₁₄ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₁₅ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₆ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → ∃ (b : α), G.IsLink e w b ∧ f w = x ∧ f b = f w_1
mpr₁₇ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₁₈ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₁₉ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → G.IsLink e w w_1 ∧ f w = x ∧ f w_1 = f w_1
mpr₂₀ mpr₂₁ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₂₂ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
mpr₂₃ : ∀ (w : α), x = f w → ∀ (w_1 : α), G.IsLink e w w_1 → G.IsLink e w w_1 ∧ f w = x ∧ f w_1 = f w_1
mpr₂₄ mpr₂₅ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α
mpr₂₆ : (w : α) → x = f w → (w_1 : α) → G.IsLink e w w_1 → α'
⊢ (∃ (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
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
obtain : ∀ (w : α) (hw : G.IsLink e v w), (map f G).Inc e (f v)
⊢ (map f G).Inc e (f v)

Tactic:
obtain ⟨w, hw⟩ := h
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
w : α
hw : G.IsLink e v w
⊢ (map f G).Inc e (f v)

Tactic:
⟨f w, hw.map f⟩

Premises used: Graph.Inc, Graph.IsLink.map, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
w : α
hw : G.IsLink e v w
⊢ (map f G).Inc e (f v)

Tactic:
exact ⟨f w, hw.map f⟩
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (map f G).IsLoopAt e x ↔ ∃ (u : α) (v : α), G.IsLink e u v ∧ f u = x ∧ f v = x

Tactic:
Iff.rfl

Premises used: Graph.IsLoopAt, Iff.rfl, Relation.Map
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.IsLoopAt e v
⊢ (map f G).IsLoopAt e (f v)

Tactic:
IsLink.map f h

Premises used: Graph.IsLoopAt, Graph.IsLink.map
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
f : α → α'
h : G.Adj u v
obtain : ∀ (e : β) (h : G.IsLink e u v), (map f G).Adj (f u) (f v)
⊢ (map f G).Adj (f u) (f v)

Tactic:
obtain ⟨e, h⟩ := h
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
f : α → α'
e : β
h : G.IsLink e u v
⊢ (map f G).Adj (f u) (f v)

Tactic:
⟨e, h.map f⟩

Premises used: Graph.Adj, Graph.IsLink.map, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
f : α → α'
e : β
h : G.IsLink e u v
⊢ (map f G).Adj (f u) (f v)

Tactic:
exact ⟨e, h.map f⟩
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
β : Type u_4
G : Graph α β
hV : ∀ (a : α), a ∈ V(map id G) ↔ a ∈ V(G)
h : ∀ (a : β) (b c : α), (map id G).IsLink a b c ↔ G.IsLink a b c
⊢ map id G = G

Tactic:
ext a b c
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
β : Type u_4
G : Graph α β
a : α
⊢ a ∈ V(map id G) ↔ a ∈ V(G)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
β : Type u_4
G : Graph α β
a : β
b c : α
⊢ (map id G).IsLink a b c ↔ G.IsLink a b c

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
hV : ∀ (a : α''), a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)
h : ∀ (a : β) (b c : α''), (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c
⊢ map f' (map f G) = map (f' ∘ f) G

Tactic:
ext a b c
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : α''
⊢ a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)

Tactic:
simp [map_apply]

Premises used: Relation.map_apply
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : β
b c : α''
⊢ (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c

Tactic:
simp [map_apply]

Premises used: Relation.map_apply
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G H : Graph α β
f : α → α'
h : G ≤ H
v : α'
⊢ v ∈ V(map f G) → v ∈ V(map f H)

Tactic:
grind [h.vertexSet_mono]

Premises used: Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G H : Graph α β
f : α → α'
hsle : G ≤s H
⊢ V(map f G) = V(map f H)

Tactic:
simp [hsle.vertexSet_eq]

Premises used: Graph.IsSpanningSubgraph.vertexSet_eq
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ V(map f G) = V(map g G)

Tactic:
grind
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
refine_1 :
  ∀ (x : β) (x_1 x_2 : α'),
    (map f G).IsLink x x_1 x_2 →
      ∀ (w w_1 : α) (hvw : G.IsLink x w w_1), f w = x_1 → f w_1 = x_2 → (map g G).IsLink x x_1 x_2
refine_2 :
  ∀ (x : β) (x_1 x_2 : α'),
    (map g G).IsLink x x_1 x_2 →
      ∀ (w w_1 : α) (hvw : G.IsLink x w w_1), g w = x_1 → g w_1 = x_2 → (map f G).IsLink x x_1 x_2
⊢ map f G = map g G

Tactic:
refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x : β
x_1 x_2 : α'
h_1 : (map f G).IsLink x x_1 x_2
w w_1 : α
hvw : G.IsLink x w w_1
left : f w = x_1
right : f w_1 = x_2
⊢ (map g G).IsLink x x_1 x_2

Tactic:
grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

Premises used: Graph.IsLink.right_mem, Graph.IsLink.left_mem, Graph.IsLink.map
-- Module: Mathlib.Combinatorics.Graph.Maps
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
x : β
x_1 x_2 : α'
h_1 : (map g G).IsLink x x_1 x_2
w w_1 : α
hvw : G.IsLink x w w_1
left : g w = x_1
right : g w_1 = x_2
⊢ (map f G).IsLink x x_1 x_2

Tactic:
grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

Premises used: Graph.IsLink.right_mem, Graph.IsLink.left_mem, Graph.IsLink.map
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ H : Graph α β
h₁ : H.IsSubgraph G
h₂ : G.IsSubgraph G₁
⊢ H.IsSubgraph G₁

Tactic:
⟨h₁.1.trans h₂.1, fun _ _ _ h ↦ h₂.2 (h₁.2 h)⟩

Premises used: Graph.IsSubgraph.mk, HasSubset.Subset.trans, Graph.IsSubgraph.isLink_mono, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h₁ : H.IsSubgraph G
h₂ : G.IsSubgraph H
⊢ H = G

Tactic:
Graph.ext (h₁.1.antisymm h₂.1) fun _ _ _ ↦ ⟨(h₁.2 ·), (h₂.2 ·)⟩

Premises used: Graph.IsSubgraph.isLink_mono, HasSubset.Subset.antisymm, Iff.intro, Graph.ext, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ H.IsSubgraph G ↔ H ≤ G

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsLink e x y
⊢ G.IsLink e x y

Tactic:
hHG.2 h

Premises used: Graph.IsSubgraph.isLink_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
he : e ∈ E(H)
obtain : ∀ (x y : α) (h' : H.IsLink e x y), e ∈ E(G)
⊢ e ∈ E(G)

Tactic:
obtain ⟨x, y, h'⟩ := exists_isLink_of_mem_edgeSet he

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
he : e ∈ E(H)
x y : α
h' : H.IsLink e x y
⊢ e ∈ E(G)

Tactic:
(h'.mono h).edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
e : β
he : e ∈ E(H)
x y : α
h' : H.IsLink e x y
⊢ e ∈ E(G)

Tactic:
exact (h'.mono h).edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
obtain : ∀ (u v : α) (huv : H.IsLink e u v), H.IsLink e x y
⊢ H.IsLink e x y

Tactic:
obtain ⟨u, v, huv⟩ := exists_isLink_of_mem_edgeSet he

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
h : G.IsLink e x y
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
inl : ∀ (h : G.IsLink e u v), H.IsLink e u v
inr : ∀ (h : G.IsLink e v u), H.IsLink e v u
⊢ H.IsLink e x y

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := (huv.mono hHG).eq_and_eq_or_eq_and_eq h

Premises used: Graph.IsLink.mono, Graph.IsLink.eq_and_eq_or_eq_and_eq, rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
h : G.IsLink e u v
⊢ H.IsLink e u v

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
h : G.IsLink e v u
⊢ H.IsLink e v u

Tactic:
huv.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
u v : α
huv : H.IsLink e u v
h : G.IsLink e v u
⊢ H.IsLink e v u

Tactic:
exact huv.symm

Premises used: Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
⊢ H.IsLink e x y ↔ G.IsLink e x y

Tactic:
⟨fun h ↦ h.mono hHG, fun h ↦ h.anti_of_mem hHG he⟩

Premises used: Graph.IsLink.mono, _private.0.Graph.IsLink.anti_of_mem, Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
h : ∀ (x y : α), H.IsLink e x y ↔ G.IsLink e x y
⊢ H.IsLink e = G.IsLink e

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x y : α
⊢ H.IsLink e x y ↔ G.IsLink e x y

Tactic:
isLink_iff hHG he

Premises used: Graph.IsSubgraph.isLink_iff
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x y : α
⊢ H.IsLink e x y ↔ G.IsLink e x y

Tactic:
exact isLink_iff hHG he

Premises used: Graph.IsSubgraph.isLink_iff
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H₁ H₂ : Graph α β
hH₁G : H₁ ≤ G
hH₂G : H₂ ≤ G
⊢ H₁.Compatible H₂

Tactic:
fun _ he₁ he₂ _ _ ↦ hH₁G.isLink_iff he₁ |>.trans <| (hH₂G.isLink_iff he₂).symm

Premises used: Graph.IsSubgraph.isLink_iff, Graph.Compatible, Iff.trans, Iff.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ H.Compatible G

Tactic:
.of_le_le hHG le_rfl

Premises used: le_rfl, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : G ≤ H
⊢ H.Compatible G

Tactic:
.of_le_le le_rfl hHG

Premises used: le_rfl, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ H : Graph α β
hG₁G : G₁ ≤ G
h : G.Compatible H
⊢ G₁.Compatible H

Tactic:
fun _ he₁ he₂ _ _ ↦ hG₁G.isLink_iff he₁ |>.trans <| h (hG₁G.edgeSet_mono he₁) he₂ ..

Premises used: Graph.IsSubgraph.isLink_iff, Graph.Compatible, Graph.IsSubgraph.edgeSet_mono, Iff.trans
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H H₁ : Graph α β
hH₁H : H₁ ≤ H
h : G.Compatible H
⊢ G.Compatible H₁

Tactic:
(h.symm.anti_left hH₁H).symm

Premises used: Graph.Compatible.anti_left, Graph.Compatible.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ H H₁ : Graph α β
hG₁G : G₁ ≤ G
hH₁H : H₁ ≤ H
h : G.Compatible H
⊢ G₁.Compatible H₁

Tactic:
(h.anti_left hG₁G).anti_right hH₁H

Premises used: Graph.Compatible.anti_right, Graph.Compatible.anti_left
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.Inc e x
⊢ G.Inc e x

Tactic:
(h.choose_spec.mono hHG).inc_left

Premises used: Graph.IsLink.mono, Exists.choose_spec, Graph.IsLink.inc_left
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
h : ∀ (x : α), H.Inc e x ↔ G.Inc e x
⊢ H.Inc e = G.Inc e

Tactic:
ext x