awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
refine_1 : Subgraph.Preconnected (V := V) (G := G) (induce ⊤ {u, v})
refine_2 : (induce ⊤ {u, v} ⊓ H).verts.Nonempty
⊢ (induce ⊤ {u, v} ⊔ H ⊔ K).Connected
have refine_3 : ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts.Nonempty
Tactic: refine Subgraph.connected_sup (Subgraph.connected_sup ?_ Hconn ?_).preconnected Kconn ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have mp : H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
mp : H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have mpr : (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) → H.Preconnected
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have mp : ∀
  (p :
    H.coe.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)),
  ∃ (p : G.Walk u v), p.toSubgraph ≤ H
Tactic: refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
⊢ ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have mp : (Walk.map H.hom p).toSubgraph ≤ H
Tactic: exists p.map (Subgraph.hom _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ H.Preconnected
have mpr : H.coe.Preconnected
Tactic: rw [Subgraph.preconnected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
⊢ H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
have mpr : ∀ (p : G.Walk u v) (h : p.toSubgraph ≤ H),
  H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)
Tactic: obtain ⟨p, h⟩ := hw hu hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have rw : H.Preconnected ∧ H.verts.Nonempty ↔
  H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
Tactic: rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw :
  H.Preconnected ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have rw₁ : (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) ∧ H.verts.Nonempty ↔
  H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
Tactic: rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw :
  H.Preconnected ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
rw₁ :
  (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
have rw₂ : (H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) ↔
  H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
Tactic: rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Preconnected ↔ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
have rw : Preconnected (V := (↑s : Type u))
    (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
  Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [induce_eq_coe_induce_top, ← Subgraph.preconnected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
rw :
  Preconnected (V := (↑s : Type u))
      (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
    Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ (induce s G).Preconnected ↔ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
have rw₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s) ↔ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [induce_eq_coe_induce_top, ← Subgraph.preconnected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Connected ↔ Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
have rw : Connected (V := (↑s : Type u))
    (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
  Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
rw :
  Connected (V := (↑s : Type u))
      (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
    Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
⊢ (induce s G).Connected ↔ Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
have rw₁ : Subgraph.Connected (G := G) (Subgraph.induce ⊤ s) ↔ Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
⊢ (induce (s ∪ t) G).Connected
have rw : Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
Tactic: rw [connected_induce_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [preconnected_induce_iff] at sconn tconn
Cleared hypotheses: sconn, tconn, sintert
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
Tactic: rw [preconnected_induce_iff] at sconn tconn
Cleared hypotheses: sconn, tconn, sintert
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ Connected (V := (↑{u, v} : Type u)) (induce {u, v} G)
have rw : Subgraph.Connected (V := V) (G := G) (Subgraph.induce ⊤ {u, v})
Tactic: rw [connected_induce_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ (SimpleGraph.induce H.verts G).Connected
have rw : Subgraph.Connected (G := G) (induce ⊤ H.verts)
Tactic: rw [connected_induce_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Connected (V := (↑{v_1 : V | v_1 ∈ p.support} : Type u)) (induce {v_1 : V | v_1 ∈ p.support} G)
have rw : (induce p.toSubgraph.verts G).Connected
Tactic: rw [← p.verts_toSubgraph]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (induce (s ∪ t) G).Connected
have rw : Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
Tactic: rw [connected_induce_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
Tactic: rw [preconnected_induce_iff] at sconn tconn
Cleared hypotheses: sconn, tconn, hv, hw, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
Tactic: rw [preconnected_induce_iff] at sconn tconn
Cleared hypotheses: sconn, tconn, hv, hw, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have hle : LE.le (α := G.Subgraph) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t)
  (Subgraph.induce ⊤ (s ∪ t))
Tactic: apply (Subgraph.connected_induce_top_sup sconn tconn hv hw ha).mono
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hle :
  LE.le (α := G.Subgraph) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t)
    (Subgraph.induce ⊤ (s ∪ t))
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
have hv₁ : Subgraph.verts (G := G) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t) =
  Subgraph.verts (G := G) (Subgraph.induce ⊤ (s ∪ t))
Tactic: apply (Subgraph.connected_induce_top_sup sconn tconn hv hw ha).mono
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ LE.le (α := G.Subgraph) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t)
    (Subgraph.induce ⊤ (s ∪ t))
have hle : G.subgraphOfAdj ha ≤ Subgraph.induce ⊤ (s ∪ t)
Tactic: simp only [sup_le_iff, Subgraph.le_induce_union_left,
      Subgraph.le_induce_union_right, and_true, ← Subgraph.subgraphOfAdj_eq_induce ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ G.subgraphOfAdj ha ≤ Subgraph.induce ⊤ (s ∪ t)
have hle : Subgraph.Adj (G := G) (Subgraph.induce ⊤ (s ∪ t)) v w
Tactic: apply subgraphOfAdj_le_of_adj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ Subgraph.verts (G := G) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t) =
    Subgraph.verts (G := G) (Subgraph.induce ⊤ (s ∪ t))
have hv₁ : {v, w} ∪ s ∪ t = s ∪ t
Tactic: simp only [Subgraph.verts_sup, Subgraph.induce_verts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ s ∪ t = s ∪ t
have hv₁ : {v, w} ∪ (s ∪ t) = s ∪ t
Tactic: rw [Set.union_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (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 s G).Connected
have rw : ∃ (v : (↑s : Type u)), ∀ (w : (↑s : Type u)), (induce s G).Reachable v w
Tactic: rw [connected_iff_exists_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (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')
⊢ ∃ (v : (↑s : Type u)), ∀ (w : (↑s : Type u)), (induce s G).Reachable v w
have refine : ∀ (w : (↑s : Type u)), (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) w
Tactic: refine ⟨⟨u, hu⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (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')
v : V
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)
have obtain : ∀ (sv : Set V) (svs : sv ⊆ s) (hu' : u ∈ sv) (hv' : v ∈ sv)
  (uv :
    (induce sv G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) u hu')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) v hv')),
  (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 ⟨sv, svs, hu', hv', uv⟩ := patches hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Sn : S.Nonempty
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
⊢ (induce (⋃₀ S) G).Connected
have obtain : ∀ (s : Set V) (sS : s ∈ S), (induce (⋃₀ S) G).Connected
Tactic: obtain ⟨s, sS⟩ := Sn
Cleared hypotheses: Sn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
⊢ (induce (⋃₀ S) G).Connected
have obtain : ∀ (v : V) (vs : v ∈ s), (induce (⋃₀ S) G).Connected
Tactic: obtain ⟨v, vs⟩ := (Sc sS).nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ (induce (⋃₀ S) G).Connected
have apply : ∀ {v_1 : V},
  v_1 ∈ ⋃₀ S →
    ∃ s' ⊆ ⋃₀ S,
      ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'),
        (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
          (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v_1 hv')
Tactic: apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' ⊆ ⋃₀ S,
    ∃ (hu' : v ∈ s') (hv' : w ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')
have hw₁ : ∃ t ∈ S, w ∈ t
Tactic: simp only [Set.mem_sUnion] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t ∈ S, w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S,
    ∃ (hu' : v ∈ s') (hv' : w ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')
have obtain : ∀ (t : Set V) (tS : t ∈ S) (wt : w ∈ t),
  ∃ s' ⊆ ⋃₀ S,
    ∃ (hu' : v ∈ s') (hv' : w ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')
Tactic: obtain ⟨t, tS, wt⟩ := hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
have obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
Tactic: obtain ⟨u, ut⟩ := tn
Cleared hypotheses: tn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
have refine_1 : ∀ (v : V) (vt : v ∈ t), Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) v
Tactic: refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
have refine_2 : (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) : Set V) G).Connected
Tactic: refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ Membership.mem (γ := Finset V) (t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) v
have refine_1 : ∃ a ∈ t, v ∈ (Nonempty.some sorry).support
Tactic: simp only [Finset.mem_biUnion, List.mem_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) G).Connected
have refine_2 : u ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) : Set V)
Tactic: apply G.induce_connected_of_patches u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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)
⊢ (induce (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V) G).Connected
have refine_2₁ : ∀ {v : V},
  v ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).support.toFinset) : Set V) →
    ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).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: apply G.induce_connected_of_patches u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some ⋯).support.toFinset) : Set V)
have refine_2 : ∃ (i : V), i ∈ t
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
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)
⊢ ∃ 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')
have hv₁ : ∃ a ∈ t, v ∈ (Nonempty.some sorry).support
Tactic: simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
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
⊢ ∃ 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')
have refine_2 : ∀ (w : V) (wt : w ∈ t) (hw : v ∈ (Nonempty.some sorry).support),
  ∃ s' ⊆ (↑(t.biUnion fun (v : V) ↦ (Nonempty.some sorry).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
Cleared hypotheses: hv