awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have ha₁ : a = v ∨ a = w
Tactic: simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
ha₁ : a = v ∨ a = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have hb₁ : b = v ∨ b = w
Tactic: simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha_1 : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha_1)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inl : ∀ (hvw : G.Adj a w) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts)
  (hb_2 : b = a ∨ b = w),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: obtain rfl | rfl := ha
Cleared hypotheses: v, hvw, ha_1, hb_1, ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha_1 : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
inl :
  ∀ (hvw : G.Adj a w) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts)
    (hb_2 : b = a ∨ b = w),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha_1)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inr : ∀ (hvw : G.Adj v a) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts)
  (hb_2 : b = v ∨ b = a),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: obtain rfl | rfl := ha
Cleared hypotheses: w, hvw, ha_1, hb_1, ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
w a b : V
hvw : G.Adj a w
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = a ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inl : ∀ (hvw : G.Adj b w) (ha hb : b ∈ (G.subgraphOfAdj hvw).verts),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: a, hvw, ha, hb_1, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
w a b : V
hvw : G.Adj a w
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = a ∨ b = w
inl :
  ∀ (hvw : G.Adj b w) (ha hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inl₁ : ∀ (hvw : G.Adj a b) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: w, hvw, ha, hb_1, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inr : ∀ (hvw : G.Adj b a) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: v, hvw, ha, hb_1, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
inr :
  ∀ (hvw : G.Adj b a) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)
have inr₁ : ∀ (hvw : G.Adj v b) (ha hb : b ∈ (G.subgraphOfAdj hvw).verts),
  (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b ha)
Tactic: obtain rfl | rfl := hb
Cleared hypotheses: a, hvw, ha, hb_1, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have inl : (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: apply Adj.reachable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have inl : (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: first | rfl | (apply Adj.reachable; simp)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have inr : (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: apply Adj.reachable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
have inr : (G.subgraphOfAdj hvw).coe.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
Tactic: first | rfl | (apply Adj.reachable; simp)
-- 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
⊢ Subgraph.Connected (V := V) (G := G) (induce ⊤ {u, v})
have rw : (G.subgraphOfAdj huv).Connected
Tactic: rw [← subgraphOfAdj_eq_induce huv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected
have rw : (H'.copy H.verts hv H'.Adj sorry).Connected
Tactic: rw [← Subgraph.copy_eq H' H.verts hv H'.Adj rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected
have refine : H.coe ≤ (H'.copy H.verts hv H'.Adj sorry).coe
Tactic: refine ⟨h.coe.mono ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ (H ⊔ K).Connected
have rw : ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
Tactic: rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
have obtain : ∀ (u : V) (hu : u ∈ H.verts) (hu' : u ∈ K.verts),
  ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
Tactic: obtain ⟨u, hu, hu'⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∃ (v : (↑(H ⊔ K).verts : Type u)), ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable v w
have exists : ∀ (w : (↑(H ⊔ K).verts : Type u)), (H ⊔ K).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (H ⊔ K).verts) u sorry) w
Tactic: exists ⟨u, Or.inl hu⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
⊢ H.degree (↑v : V) = 0 ↔ H.verts.Subsingleton
have refine : ∀ (hv : H.degree (↑v : V) = 0) (hn : H.verts.Nontrivial), False
Tactic: refine ⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : (↑H.verts : Type u)
inst : Fintype (↑(H.neighborSet (↑v : V)) : Type u)
hv : H.degree (↑v : V) = 0
hn : H.verts.Nontrivial
⊢ False
have this : Nontrivial.{u} (↑H.verts : Type u)
Tactic: have := hn.coe_sort
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
⊢ ∃ (u : V), H.Adj (↑v : V) u
have this : ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u
Tactic: have := h.coe.exists_adj_of_nontrivial v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
this : ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u
⊢ ∃ (u : V), H.Adj (↑v : V) u
have tauto : ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → ∃ (u : V), H.Adj (↑v : V) u
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
this : ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → ∃ (u : V), H.Adj (↑v : V) u
⊢ ∃ (u : V), H.Adj (↑v : V) u
have h₁ : ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → H.Adj (↑v : V) (↑w : V)
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
inst : Nontrivial.{u} (↑H.verts : Type u)
h : H.Preconnected
v : (↑H.verts : Type u)
this : ∃ (u : (↑H.verts : Type u)), H.coe.Adj v u
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → ∃ (u : V), H.Adj (↑v : V) u
h₁ : ∀ (w : (↑H.verts : Type u)), H.coe.Adj v w → H.Adj (↑v : V) (↑w : V)
⊢ ∃ (u : V), H.Adj (↑v : V) u
have w : (w : (↑H.verts : Type u)) → H.coe.Adj v w → V
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ (c : G.ConnectedComponent), H.verts = c.supp
have rw : ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
Tactic: rw [SimpleGraph.ConnectedComponent.exists]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
have obtain : ∀ (v : V) (hv : v ∈ H.verts), ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
Tactic: obtain ⟨v, hv⟩ := hc.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ ∃ (v : V), H.verts = (G.connectedComponentMk v).supp
have h₁ : H.verts = (G.connectedComponentMk v).supp
Tactic: use v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ H.verts = (G.connectedComponentMk v).supp
have h₁ : ∀ (w : V), w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp
have h₁ : w ∈ H.verts ↔ G.Reachable w v
Tactic: simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal Subgraph.Connected C.toSubgraph
have refine : ∀ (v : V) (G' : G.Subgraph) (hconn : G'.Connected) (hle : (G.connectedComponentMk v).toSubgraph ≤ G'),
  G' ≤ (G.connectedComponentMk v).toSubgraph
Tactic: refine C.ind fun v ↦ ⟨connected_toSubgraph _, fun G' hconn hle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph
have refine : ∀ (u : V) (hu : u ∈ G'.verts), u ∈ (G.connectedComponentMk v).supp
Tactic: refine le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Maximal Subgraph.Connected G' ↔ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
have refine_1 : Maximal Subgraph.Connected G' →
  ∀ (hconn : G'.Connected) (h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'),
    ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
Tactic: refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
refine_1 :
  Maximal Subgraph.Connected G' →
    ∀ (hconn : G'.Connected) (h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'),
      ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
⊢ Maximal Subgraph.Connected G' ↔ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
have refine_2 : (∃ (C : G.ConnectedComponent), C.toSubgraph = G') →
  ∀ (C : G.ConnectedComponent) (h : C.toSubgraph = G'), Maximal Subgraph.Connected G'
Tactic: refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
⊢ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
have refine_1 : ∀ (v : V) (hv : v ∈ G'.verts), ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
Tactic: have ⟨v, hv⟩ := hconn.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
h_1 : Maximal Subgraph.Connected G'
hconn : G'.Connected
h : ∀ ⦃y : G.Subgraph⦄, y.Connected → G' ≤ y → y ≤ G'
v : V
hv : v ∈ G'.verts
⊢ ∃ (C : G.ConnectedComponent), C.toSubgraph = G'
have refine_1 : G' ≤ (G.connectedComponentMk v).toSubgraph
Tactic: suffices G' ≤ (G.connectedComponentMk v).toSubgraph from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSubgraph _) this) this⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support
have this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
Tactic: have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.toSubgraph.verts ↔ w ∈ p.support
have nil : ∀ {u : V},
  Membership.mem (γ := Set V) (Subgraph.verts (G := G) (Walk.toSubgraph (u := u) nil)) w ↔
    Membership.mem (γ := List V) (support (G := G) (u := u) nil) w
Tactic: induction p with
  | nil => simp
  | cons h p' ih =>
    rename_i x y z
    have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
    simp [ih, or_assoc, this]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Membership.mem (γ := Set V) (Subgraph.verts (G := G) (Walk.toSubgraph (u := u) Walk.nil)) w ↔
      Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w
⊢ w ∈ p.toSubgraph.verts ↔ w ∈ p.support
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p' : G.Walk v w_1) (ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support),
  w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support
Tactic: induction p with
  | nil => simp
  | cons h p' ih =>
    rename_i x y z
    have : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support :=
      ⟨by rintro (rfl | h) <;> simp [*], by simp +contextual⟩
    simp [ih, or_assoc, this]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
⊢ ¬p.Nil
have nil : ∀ (hadj : Subgraph.Adj (G := G) (Walk.toSubgraph (u := u) nil) w x), ¬Nil.{u} (V := V) (G := G) (v := u) nil
Tactic: cases p
Cleared hypotheses: v, p, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
nil :
  ∀ (hadj : Subgraph.Adj (G := G) (Walk.toSubgraph (u := u) Walk.nil) w x), ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil
⊢ ¬p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (hadj : (cons h p).toSubgraph.Adj w x), ¬(cons h p).Nil
Tactic: cases p
Cleared hypotheses: p, hadj
-- 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
e : Sym2 V
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
have nil : ∀ {u : V},
  Membership.mem (γ := Set (Sym2 V)) (Subgraph.edgeSet (G := G) (Walk.toSubgraph (u := u) nil)) e ↔
    Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e
Tactic: induction p
Cleared hypotheses: p
-- 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
e : Sym2 V
nil :
  ∀ {u : V},
    Membership.mem (γ := Set (Sym2 V)) (Subgraph.edgeSet (G := G) (Walk.toSubgraph (u := u) Walk.nil)) e ↔
      Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges) → (e ∈ (cons h p).toSubgraph.edgeSet ↔ e ∈ (cons h p).edges)
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
have nil : ∀ {u : V} (q : G.Walk u w), (append nil q).toSubgraph = Walk.toSubgraph (u := u) nil ⊔ q.toSubgraph
Tactic: induction p
Cleared hypotheses: p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
nil : ∀ {u : V} (q : G.Walk u w), (append Walk.nil q).toSubgraph = Walk.toSubgraph (u := u) Walk.nil ⊔ q.toSubgraph
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (q : G.Walk w_1 w), (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph) →
    ∀ (q : G.Walk w_1 w), ((cons h p).append q).toSubgraph = (cons h p).toSubgraph ⊔ q.toSubgraph
Tactic: induction p
Cleared hypotheses: p, q