awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected

Tactic:
⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩

Premises used: SimpleGraph.Walk.support, Nonempty.some, Finset.biUnion, List.toFinset, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
refine_1 :
  ∀ (v : V) (vt : v ∈ t), Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) v
refine_2 : (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) G).Connected
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected

Tactic:
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
refine_1 : ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support
⊢ Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) v

Tactic:
simp only [Finset.mem_biUnion, List.mem_toFinset]

Premises used: List.mem_toFinset, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Tactic:
⟨v, vt, Walk.end_mem_support _⟩

Premises used: SimpleGraph.Walk.end_mem_support, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Tactic:
exact ⟨v, vt, Walk.end_mem_support _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
refine_2 : u ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
refine_2₁ :
  ∀ {v : V},
    v ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) →
      ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
⊢ (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) G).Connected

Tactic:
apply G.induce_connected_of_patches u

Premises used: SimpleGraph.induce_connected_of_patches
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
refine_2 : ∃ (i : V), i ∈ t
⊢ u ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]

Premises used: Finset.coe_biUnion, and_true, SimpleGraph.Walk.start_mem_support, List.coe_toFinset, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ (i : V), i ∈ t

Tactic:
⟨u, ut⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ (i : V), i ∈ t

Tactic:
exact ⟨u, ut⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Tactic:
simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv

Premises used: List.mem_toFinset, Finset.mem_coe, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support
refine_2 :
  ∀ (w : V) (wt : w ∈ t) (hw : v ∈ (Nonempty.some ⋯).support),
    ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
      ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
        (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
          (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
⊢ ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')

Tactic:
obtain ⟨w, wt, hw⟩ := hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')

Tactic:
⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩

Premises used: setOf, SimpleGraph.Walk.support, Membership.mem, Nonempty.some, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
refine_2 :
  {x : V | x ∈ (Nonempty.some ⋯).support} ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
refine_2₁ :
  ∃ (hu' : Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} u) (hv' :
    Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} v),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) u hu')
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) v hv')
⊢ ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')

Tactic:
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
refine_2 :
  Subset.{u} (α := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} (⋃ x ∈ t, {a : V | a ∈ (Nonempty.some ⋯).support})
⊢ {x : V | x ∈ (Nonempty.some ⋯).support} ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]

Premises used: Finset.coe_biUnion, List.coe_toFinset, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ Subset.{u} (α := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} (⋃ x ∈ t, {a : V | a ∈ (Nonempty.some ⋯).support})

Tactic:
fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Set.Subset, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ Subset.{u} (α := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} (⋃ x ∈ t, {a : V | a ∈ (Nonempty.some ⋯).support})

Tactic:
exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
refine_2 :
  ∃ (h : v ∈ (Nonempty.some ⋯).support),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) u ⋯)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) v ⋯)
⊢ ∃ (hu' : Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} u) (hv' :
    Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} v),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) u hu')
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {x : V | x ∈ (Nonempty.some ⋯).support} x) v hv')

Tactic:
simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]

Premises used: SimpleGraph.Walk.start_mem_support, exists_true_left, Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (h : v ∈ (Nonempty.some ⋯).support),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) u ⋯)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) v ⋯)

Tactic:
⟨hw, Walk.connected_induce_support _ _ _⟩

Premises used: SimpleGraph.Connected.preconnected, Exists.intro, SimpleGraph.Walk.connected_induce_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (h : v ∈ (Nonempty.some ⋯).support),
    Reachable (induce {x : V | x ∈ (Nonempty.some ⋯).support} G)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) u ⋯)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Nonempty.some ⋯).support) v ⋯)

Tactic:
refine ⟨hw, Walk.connected_induce_support _ _ _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
refine_1 :
  ∀ (u : V) (ut : u ∈ t) (v : V) (vt : v ∈ t),
    Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) v
refine_2 refine_2₁ :
  ∀ (u : V) (ut : u ∈ t), (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) G).Connected
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected

Tactic:
classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

Premises used: List.mem_toFinset, Finset.coe_biUnion, and_true, SimpleGraph.Walk.start_mem_support, List.coe_toFinset, exists_true_left, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop, Finset.mem_coe, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
u v : V
h : H ≤ G
hreachable : H.Reachable u v
⊢ (toSubgraph H h).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (toSubgraph H h).verts) u trivial)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (toSubgraph H h).verts) v trivial)

Tactic:
hreachable.map ⟨((toSubgraph H h).vert · _), (·)⟩

Premises used: SimpleGraph.toSubgraph, SimpleGraph.Reachable.map, RelHom.mk, SimpleGraph.Subgraph.vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
hpreconn : H.Preconnected
⊢ (toSubgraph H h).Preconnected

Tactic:
Subgraph.preconnected_iff.mpr (fun u v ↦ (hpreconn u v).coe_toSubgraph h)

Premises used: Iff.mpr, SimpleGraph.Subgraph.preconnected_iff, SimpleGraph.Reachable.coe_toSubgraph, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
hconn : H.Connected
⊢ (toSubgraph H h).verts.Nonempty

Tactic:
simp [hconn.nonempty]

Premises used: SimpleGraph.Connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
a b : (↑G''.verts : Type u)
r : G''.coe.Adj a b
h :
  ∃ (b_1 : (↑G'.verts : Type u)),
    G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
w : (↑G'.verts : Type u)
h₁ :
  ∃ (b_1 : (↑G'.verts : Type u)),
    G''.Adj (↑a : (↑G'.verts : Type u)) b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
w₁ : (↑G'.verts : Type u)
h₂ :
  G''.Adj (↑a : (↑G'.verts : Type u)) (↑b : (↑G'.verts : Type u)) ∧
    (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u)) =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
h₃ w₂ : (↑G'.verts : Type u)
h₄ :
  G''.Adj (↑a : (↑G'.verts : Type u)) (↑b : (↑G'.verts : Type u)) ∧
    (f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u)) =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
      (f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u)) =
        (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)
h₅ w₃ : (↑G'.verts : Type u)
⊢ ∃ (a_1 : (↑G'.verts : Type u)) (b_1 : (↑G'.verts : Type u)),
    G''.Adj a_1 b_1 ∧
      (f : (a : (↑G'.verts : Type u)) → V) a_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑a : (↑G'.verts : Type u))) ⋯) : V) ∧
        (f : (a : (↑G'.verts : Type u)) → V) b_1 =
          (↑((Subgraph.map f G'').vert ((f : (a : (↑G'.verts : Type u)) → V) (↑b : (↑G'.verts : Type u))) ⋯) : V)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G'_1 : SimpleGraph V'
G' : G.Subgraph
G'' : G'.coe.Subgraph
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
⊢ (↑(↑u : (↑G'.verts : Type u)) : V) ∈ (Subgraph.coeSubgraph G'').verts

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G'_1 : SimpleGraph V'
G' : G.Subgraph
G'' : G'.coe.Subgraph
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
⊢ (↑(↑v : (↑G'.verts : Type u)) : V) ∈ (Subgraph.coeSubgraph G'').verts

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
u v : (↑G''.verts : Type u)
hreachable : G''.coe.Reachable u v
⊢ (Subgraph.coeSubgraph G'').coe.Reachable ((Subgraph.coeSubgraph G'').vert (↑(↑u : (↑G'.verts : Type u)) : V) ⋯)
    ((Subgraph.coeSubgraph G'').vert (↑(↑v : (↑G'.verts : Type u)) : V) ⋯)

Tactic:
hreachable.coe_subgraphMap G'.hom

Premises used: Set.Mem, SimpleGraph.Subgraph.hom, SimpleGraph.Reachable.coe_subgraphMap
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
rw : (Subgraph.map f G'').coe.Preconnected
⊢ (Subgraph.map f G'').Preconnected

Tactic:
rw [Subgraph.preconnected_iff]

Premises used: SimpleGraph.Subgraph.preconnected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
this :
  ∀ (v' : V) (v : (↑G'.verts : Type u)) (hv : v ∈ G''.verts) (hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'),
    (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' ⋯)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) v' ⋯)
⊢ ∀ (v : (↑(Subgraph.map f G'').verts : Type u)),
    (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' ⋯) v

Tactic:
⟨v', v, hv, hfv⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
v' : V
v : (↑G'.verts : Type u)
hv : v ∈ G''.verts
hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'
simp_rw :
  (Subgraph.map f G'').coe.Reachable
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) u) ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) v) ⋯)
⊢ (Subgraph.map f G'').coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) u' ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) v' ⋯)

Tactic:
simp_rw [← hfu, ← hfv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
v' : V
v : (↑G'.verts : Type u)
hv : v ∈ G''.verts
hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'
⊢ (Subgraph.map f G'').coe.Reachable
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) u) ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) v) ⋯)

Tactic:
(hpreconn.coe ⟨u, hu⟩ ⟨v, hv⟩).coe_subgraphMap f

Premises used: SimpleGraph.Subgraph.Preconnected.coe, Subtype.mk, SimpleGraph.Reachable.coe_subgraphMap
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : (↑G'.verts : Type u)
hu : u ∈ G''.verts
hfu : (f : (a : (↑G'.verts : Type u)) → V) u = u'
v' : V
v : (↑G'.verts : Type u)
hv : v ∈ G''.verts
hfv : (f : (a : (↑G'.verts : Type u)) → V) v = v'
⊢ (Subgraph.map f G'').coe.Reachable
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) u) ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (Subgraph.map f G'').verts) ((f : (a : (↑G'.verts : Type u)) → V) v) ⋯)

Tactic:
exact (hpreconn.coe ⟨u, hu⟩ ⟨v, hv⟩).coe_subgraphMap f

Premises used: SimpleGraph.Subgraph.Preconnected.coe, Subtype.mk, SimpleGraph.Reachable.coe_subgraphMap
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hconn : G''.Connected
⊢ (Subgraph.map f G'').verts.Nonempty

Tactic:
simp [hconn.nonempty]

Premises used: SimpleGraph.Subgraph.Connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
hpreconn : G''.Preconnected
⊢ (Subgraph.coeSubgraph G'').Preconnected

Tactic:
hpreconn.map G'.hom

Premises used: SimpleGraph.Subgraph.Preconnected.map, SimpleGraph.Subgraph.hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
hconn : G''.Connected
⊢ (Subgraph.coeSubgraph G'').Connected

Tactic:
hconn.map G'.hom

Premises used: SimpleGraph.Subgraph.Connected.map, SimpleGraph.Subgraph.hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f g : A.Copy B
h :
  Eq (α := (a : α) → β) ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) f)
    ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) g)
obtain :
  ∀ (toFun : α → β) (map_rel' : ∀ {a b : α}, A.Adj a b → B.Adj (toFun a) (toFun b))
    (injective' :
      Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β)
        (⇑(RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel') : (a : α) → β))
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β))
          { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' })
        ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) g)),
    { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' : A.Copy B } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : A.Copy B
toFun : α → β
map_rel' : ∀ {a b : α}, A.Adj a b → B.Adj (toFun a) (toFun b)
injective' :
  Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑(RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel') : (a : α) → β)
h :
  Eq (α := (a : α) → β)
    ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β))
      { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' })
    ((fun (f : A.Copy B) ↦ ((⇑f.toHom : (a : α) → β) : (a : α) → β)) g)
⊢ { toHom := RelHom.mk (r := A.Adj) (s := B.Adj) toFun @map_rel', injective' := injective' : A.Copy B } = g

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
⊢ Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f.toHom : (a : α) → β)

Tactic:
f.injective'

Premises used: SimpleGraph.Copy.injective'
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f g : A.Copy B
⊢ (∀ (a : α), Eq.{u_5 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
⊢ Eq (α := (a : α) → β) (⇑f.toHom : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl