awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
p : G.Walk u v := Classical.choice h
⊢ u ∈ G.support
have hp : ¬p.Nil
Tactic: have hp : ¬p.Nil := Walk.not_nil_of_ne huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Connected ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w
have rw : G.Preconnected ∧ Nonempty V ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w
Tactic: rw [connected_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w
have mp : G.Preconnected ∧ Nonempty V → ∃ (v : V), ∀ (w : V), G.Reachable v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
mp : G.Preconnected ∧ Nonempty V → ∃ (v : V), ∀ (w : V), G.Reachable v w
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w
have mpr : (∃ (v : V), ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
⊢ G.Reachable u v ∨ Gᶜ.Reachable u w
have refine : ∀ (huv : ¬G.Reachable u v), Gᶜ.Reachable u w
Tactic: refine or_iff_not_imp_left.mpr fun huv ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
⊢ Gᶜ.Reachable u w
have pos : ∀ (huw : G.Reachable u w), Gᶜ.Reachable u w
Tactic: by_cases huw : G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
pos : ∀ (huw : G.Reachable u w), Gᶜ.Reachable u w
⊢ Gᶜ.Reachable u w
have neg : ∀ (huw : ¬G.Reachable u w), Gᶜ.Reachable u w
Tactic: by_cases huw : G.Reachable u w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
⊢ Gᶜ.Reachable u w
have huv' : Gᶜ.Adj u v
Tactic: have huv' := G.reachable_or_compl_adj .. |>.resolve_left huv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
⊢ Gᶜ.Reachable u w
have hvw' : Gᶜ.Adj v w
Tactic: have hvw' := G.reachable_or_compl_adj .. |>.resolve_left fun hvw ↦ huv <| huw.trans hvw.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Connected ∨ Gᶜ.Preconnected
have rw : (¬∃ (v : V), ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected
Tactic: rw [or_iff_not_imp_left, G.connected_iff_exists_forall_reachable]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
h : ¬∃ (v : V), ∀ (w : V), G.Reachable v w
u v : V
⊢ Gᶜ.Reachable u v
have h₁ : ∀ (v : V), ∃ (w : V), ¬G.Reachable v w
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ∀ (v : V), ∃ (w : V), ¬G.Reachable v w
⊢ Gᶜ.Reachable u v
have have : ∀ (w : V) (huw : ¬G.Reachable u w), Gᶜ.Reachable u v
Tactic: have ⟨w, huw⟩ := h u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v : V
C : G.ConnectedComponent
⊢ G'.connectedComponentMk ((φ : (a : V) → V') v) =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C ↔
    G.connectedComponentMk v = C
have refine : ∀ (u : V),
  G'.connectedComponentMk ((φ : (a : V) → V') v) =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj))
        (G.connectedComponentMk u) ↔
    G.connectedComponentMk v = G.connectedComponentMk u
Tactic: refine C.ind fun u => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v' : V'
C : G.ConnectedComponent
⊢ G.connectedComponentMk ((φ.symm : (a : V') → V) v') = C ↔
    G'.connectedComponentMk v' =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C
have refine : ∀ (u : V),
  G.connectedComponentMk ((φ.symm : (a : V') → V) v') = G.connectedComponentMk u ↔
    G'.connectedComponentMk v' =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj))
        (G.connectedComponentMk u)
Tactic: refine C.ind fun u => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := G.ConnectedComponent ≃ G.ConnectedComponent) (connectedComponentEquiv refl)
    (Equiv.refl G.ConnectedComponent)
have H : ∀ (x : G.ConnectedComponent) (v : V),
  Eq (α := G.ConnectedComponent)
    ((connectedComponentEquiv refl : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
      G.ConnectedComponent)
    ((Equiv.refl G.ConnectedComponent : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
      G.ConnectedComponent)
Tactic: ext ⟨v⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
⊢ φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm
have H : ∀ (x : G'.ConnectedComponent) (a : V'),
  Eq.{u + 1} (α := G.ConnectedComponent)
    ((φ.symm.connectedComponentEquiv : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
      G.ConnectedComponent)
    ((φ.connectedComponentEquiv.symm : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
      G.ConnectedComponent)
Tactic: ext ⟨_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
⊢ connectedComponentEquiv (RelIso.trans (r := G.Adj) (s := G'.Adj) (t := G''.Adj) φ φ') =
    φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv
have H : ∀ (x : G.ConnectedComponent) (a : V),
  Eq.{w + 1} (α := G''.ConnectedComponent)
    ((connectedComponentEquiv (RelIso.trans (r := G.Adj) (s := G'.Adj) (t := G''.Adj) φ φ') :
          (a : G.ConnectedComponent) → G''.ConnectedComponent)
        (Quot.mk G.Reachable a) :
      G''.ConnectedComponent)
    ((φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv : (a : G.ConnectedComponent) → G''.ConnectedComponent)
        (Quot.mk G.Reachable a) :
      G''.ConnectedComponent)
Tactic: ext ⟨_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ Injective.{u + 1, u + 1} (α := G.ConnectedComponent) supp
have refine : ∀ (v w : V),
  (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
    G.connectedComponentMk v = G.connectedComponentMk w
Tactic: refine ConnectedComponent.ind₂ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w
have simp : ∀ (v w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w
Tactic: simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable v w
have rw : G.Reachable w v
Tactic: rw [reachable_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
rw : G.Reachable w v
⊢ G.Reachable v w
have rw₁ : G.Reachable w w
Tactic: rw [reachable_comm, h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c
have mp : G.connectedComponentMk v = c → G.connectedComponentMk w = c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
mp : G.connectedComponentMk v = c → G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c
have mpr : G.connectedComponentMk w = c → G.connectedComponentMk v = c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = c
have mp : G.connectedComponentMk w = G.connectedComponentMk v
Tactic: simp only [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = c
have mpr : G.connectedComponentMk v = G.connectedComponentMk w
Tactic: simp only [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = G.connectedComponentMk v
have mp : G.Adj w v
Tactic: apply connectedComponentMk_eq_of_adj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
hw : w ∈ H.verts
hadj : H.Adj v w
⊢ w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
have obtain : ∀ (w_1 : (↑H.verts : Type u)) (h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v),
  w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
Tactic: obtain ⟨_, h⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
⊢ w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
have h₁ : Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑c : Set (↑H.verts : Type u)) ∧
  (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w
Tactic: use ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑c : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w
have h₁ : Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑(H.coe.connectedComponentMk w_1) : Set (↑H.verts : Type u)) ∧
  (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w
Tactic: rw [← (mem_supp_iff _ _).mp h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
⊢ c = c'
have hc₁ : G.connectedComponentMk v = c
Tactic: simp only [mem_supp_iff] at *
Cleared hypotheses: hc, hc'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
hc₁ : G.connectedComponentMk v = c
⊢ c = c'
have hc'₁ : G.connectedComponentMk v = c'
Tactic: simp only [mem_supp_iff] at *
Cleared hypotheses: hc, hc'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' rw : G.connectedComponentMk v = c'
⊢ c = c'
have rw₁ : G.connectedComponentMk v = G.connectedComponentMk v
Tactic: rw [← hc, ← hc']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : v' ∈ (G.connectedComponentMk v).supp
⊢ v' ∈ c'.supp
have hv'₁ : G.Reachable v' v
Tactic: simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v' = c'
have rw : G'.connectedComponentMk v = c'
Tactic: rw [ConnectedComponent.sound (hv'.mono h)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ ⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp
have h₁ : ∀ (v : V), Membership.mem (γ := Set V) (⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp) v ↔ v ∈ c'.supp
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ Membership.mem (γ := Set V) (⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp) v ↔ v ∈ c'.supp
have h₁ : (∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp
Tactic: simp_rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp
have h₁ : v ∈ c'.supp → ∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp
Tactic: refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp
have h₁ : ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp
Tactic: use G.connectedComponentMk v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp
have h₁ : v ∈ (G.connectedComponentMk v).supp
Tactic: use c'.connectedComponentMk_supp_subset_supp h hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
c : ConnectedComponent (V := V) ⊤
⊢ c.supp = Set.univ
have obtain : ∀ (w : V), supp (G := ⊤) (Quot.mk (Reachable ⊤) w) = Set.univ
Tactic: obtain ⟨w, rfl⟩ := c.exists_rep
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
w : V
⊢ supp (G := ⊤) (Quot.mk (Reachable ⊤) w) = Set.univ
have h : ∀ (v : V), v ∈ supp (G := ⊤) (Quot.mk (Reachable ⊤) w) ↔ Membership.mem (γ := Set V) Set.univ v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hv : v ∈ C.supp
⊢ G.Reachable u v
have hu₁ : G.connectedComponentMk u = C
Tactic: rw [mem_supp_iff] at hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hv : v ∈ C.supp
hu₁ : G.connectedComponentMk u = C
⊢ G.Reachable u v
have hv₁ : G.connectedComponentMk v = C
Tactic: rw [mem_supp_iff] at hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w ↔ v ∈ C.supp ∧ G.Adj v w
have mp : C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w → v ∈ C.supp ∧ G.Adj v w
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
mp : C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w → v ∈ C.supp ∧ G.Adj v w
⊢ C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w ↔ v ∈ C.supp ∧ G.Adj v w
have mpr : v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h : C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w
⊢ v ∈ C.supp ∧ G.Adj v w
have h₁ : ∃ (a : V) (b : a ∈ C) (a_1 : V) (b_1 : a_1 ∈ C),
  C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) ∧
    (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) = v ∧
      (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
          (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) =
        w
Tactic: simp_all only [map_adj, SetLike.coe_sort_coe, Subtype.exists, mem_supp_iff]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h :
  ∃ (a : V) (b : a ∈ C) (a_1 : V) (b_1 : a_1 ∈ C),
    C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) ∧
      (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) =
          v ∧
        (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
            (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) =
          w
⊢ G.connectedComponentMk v = C ∧ G.Adj v w
have mp : ∀ (w : V) (a : w ∈ C) (w_1 : V) (w_2 : w_1 ∈ C)
  (h₁ :
    C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w_1 w_2)),
  G.connectedComponentMk
        ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
          (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a)) =
      C ∧
    G.Adj
      ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a))
      ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
        (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w_1 w_2))
Tactic: obtain ⟨_, a, _, _, h₁, rfl, rfl⟩ := h
Cleared hypotheses: v, w, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w
have mpr : v ∈ C.supp →
  G.Adj v w → ∃ (a : V) (_ : a ∈ (↑C : Set V)) (a_1 : V), G.Adj a a_1 ∧ a = v ∧ ∃ (_ : a_1 ∈ (↑C : Set V)), a_1 = w
Tactic: simp only [toSimpleGraph, map_adj, comap_adj, Embedding.subtype_apply, Subtype.exists,
      exists_and_left, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
have hw : w ∈ C
Tactic: have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
have h' : C.toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) w hw)
Tactic: have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
p : G.Walk u v
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
have nil : (hv : u ∈ C) →
  C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hv)
Tactic: cases p with
  | nil => exact Walk.nil
  | @cons v w u h p =>
    have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
    have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
    exact Walk.cons h' (C.walk_toSimpleGraph hw hv p)
Cleared hypotheses: v, hv, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
p : G.Walk u v
nil :
  (hv : u ∈ C) →
    C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hv)
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
have cons : {w : V} →
  (h : G.Adj u w) →
    (p : G.Walk w v) →
      C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
Tactic: cases p with
  | nil => exact Walk.nil
  | @cons v w u h p =>
    have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
    have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
    exact Walk.cons h' (C.walk_toSimpleGraph hw hv p)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
⊢ ∀ (v : ↥C), C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) v
have this : ∀ (v : V) (hv : v ∈ C),
  C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
Tactic: ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) C.supp
have refine : ∀ (v : V), Maximal (fun (x : Set V) ↦ (induce x G).Connected) (G.connectedComponentMk v).supp
Tactic: refine C.ind fun v ↦ ?_