awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) (G.connectedComponentMk v).supp
have refine : ∀ (s : Set V) (hconn : (fun (x : Set V) ↦ (induce x G).Connected) s) (hle : (G.connectedComponentMk v).supp ≤ s) (u : V)
  (hu : u ∈ s), G.Reachable u v
Tactic: refine ⟨connected_toSimpleGraph _, fun s hconn hle u hu ↦ ConnectedComponent.sound ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s ↔ ∃ (C : G.ConnectedComponent), C.supp = s
have refine_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s →
  ∀ (hconn : (induce s G).Connected) (h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s),
    ∃ (C : G.ConnectedComponent), C.supp = s
Tactic: refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
refine_1 :
  Maximal (fun (x : Set V) ↦ (induce x G).Connected) s →
    ∀ (hconn : (induce s G).Connected)
      (h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s),
      ∃ (C : G.ConnectedComponent), C.supp = s
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s ↔ ∃ (C : G.ConnectedComponent), C.supp = s
have refine_2 : (∃ (C : G.ConnectedComponent), C.supp = s) →
  ∀ (C : G.ConnectedComponent) (h : C.supp = s), Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
Tactic: refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
⊢ ∃ (C : G.ConnectedComponent), C.supp = s
have refine_1 : ∀ (v : V) (hv : v ∈ s), ∃ (C : G.ConnectedComponent), C.supp = s
Tactic: have ⟨v, hv⟩ := hconn.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
v : V
hv : v ∈ s
⊢ ∃ (C : G.ConnectedComponent), C.supp = s
have refine_1 : s ≤ (G.connectedComponentMk v).supp
Tactic: suffices s ≤ (G.connectedComponentMk v).supp from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSimpleGraph _) this) this⟩
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h : (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a sorry)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b sorry)
Tactic: have h : (G.connectedComponentMk _).toSimpleGraph.Adj ⟨_, rfl⟩
        ⟨_, ((G.connectedComponentMk _).mem_supp_congr_adj hab).1 rfl⟩ := by simpa using hab
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
Tactic: convert! (C (G.connectedComponentMk _)).map_rel h using 3
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h₂ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
Tactic: convert! (C (G.connectedComponentMk _)).map_rel h using 3
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
h₂ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h₃ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
  ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
    (HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
        outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V') →
      ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
        (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj
Tactic: convert! (C (G.connectedComponentMk _)).map_rel h using 3
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
h₂ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
h₃ :
  ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
    ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
      (HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
          outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V') →
        ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
          (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h₄ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
  G.connectedComponentMk b = G.connectedComponentMk a
Tactic: convert! (C (G.connectedComponentMk _)).map_rel h using 3
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
h₂ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
h₃ :
  ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
    ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
      (HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
          outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V') →
        ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
          (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj
h₄ :
  ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
    G.connectedComponentMk b = G.connectedComponentMk a
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))
have h₅ : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
  Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
Tactic: convert! (C (G.connectedComponentMk _)).map_rel h using 3
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
⊢ ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
have h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk b).toSimpleGraph.Adj →r H.Adj)
Tactic: rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
⊢ Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
have h₁ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk b
Tactic: rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_1 : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
e_2 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
e_3 :
  HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
    outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V'
e_1_1 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
⊢ (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj
have h₁ : (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk b).toSimpleGraph.Adj
Tactic: rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_1 : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b = G.connectedComponentMk a
have h₁ : G.connectedComponentMk b = G.connectedComponentMk b
Tactic: rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]
-- 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
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_2 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
⊢ Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
have h₁ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk b
Tactic: rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ Pairwise fun (c c' : G.ConnectedComponent) ↦ Disjoint c.supp c'.supp
have simp_rw : Pairwise fun (c c' : G.ConnectedComponent) ↦ ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp
Tactic: simp_rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : a ∈ i.supp
hsy : a ∈ j.supp
⊢ False
have hsx₁ : G.connectedComponentMk a = i
Tactic: rw [ConnectedComponent.mem_supp_iff] at hsx hsy
Cleared hypotheses: hsx, hsy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : a ∈ i.supp
hsy : a ∈ j.supp
hsx₁ : G.connectedComponentMk a = i
⊢ False
have hsy₁ : G.connectedComponentMk a = j
Tactic: rw [ConnectedComponent.mem_supp_iff] at hsx hsy
Cleared hypotheses: hsx, hsy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : G.connectedComponentMk a = i
hsy : G.connectedComponentMk a = j
⊢ False
have hsy₁ : i = j
Tactic: rw [hsx] at hsy
Cleared hypotheses: hsy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := Set V) (⋃ (c : G.ConnectedComponent), c.supp) Set.univ
have refine : ∀ (v : V),
  Membership.mem (γ := Set (Set V)) (Set.range fun (c : G.ConnectedComponent) ↦ c.supp)
      (↑(G.connectedComponentMk v) : Set V) ∧
    v ∈ (↑(G.connectedComponentMk v) : Set V)
Tactic: refine Set.eq_univ_of_forall fun v ↦ ⟨G.connectedComponentMk v, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Set.Nonempty.{u} (α := G.Walk u v) Set.univ
have rw : Nonempty.{u + 1} (G.Walk u v)
Tactic: rw [← Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
⊢ ∃ (u : V), G.Adj v u
have have : ∀ (u : V) (huv : u ≠ v), ∃ (u : V), G.Adj v u
Tactic: have ⟨u, huv⟩ := exists_ne v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v u : V
huv : u ≠ v
⊢ ∃ (u : V), G.Adj v u
have have : ∀ (w : G.Walk v u), ∃ (u : V), G.Adj v u
Tactic: have ⟨w⟩ := h v u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
he : G.IsBridge e
⊢ Nontrivial V
have h : ∀ (u v : V) (he : G.IsBridge s(u, v)), Nontrivial V
Tactic: cases e with | h u v
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
have mp : (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
mp : (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
have mpr : (∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ∃ (p : G.Walk v' w'), s(v, w) ∉ p.edges
have h : s(v, w) ∉
  Walk.edges (u := v') (v := w')
    (Walk.map (Hom.ofLE sorry) p : G.Walk ((Hom.ofLE sorry : (a : V) → V) v') ((Hom.ofLE sorry : (a : V) → V) w'))
Tactic: use p.map (.ofLE (by simp))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉
    Walk.edges (u := v') (v := w')
      (Walk.map (Hom.ofLE ⋯) p : G.Walk ((Hom.ofLE ⋯ : (a : V) → V) v') ((Hom.ofLE ⋯ : (a : V) → V) w'))
have h : ¬∃ a ∈ p.edges, a = s(v, w)
Tactic: simp_rw [Walk.edges_map, List.mem_map, Hom.ofLE_apply, Sym2.map_id', id]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w'
have mpr : ∀ (e : Sym2 V) (ep : e ∈ p.edges), e ∈ (G.deleteEdges {s(v, w)}).edgeSet
Tactic: refine ⟨p.transfer _ fun e ep => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ (G.deleteEdges {s(v, w)}).edgeSet
have mpr : e ∈ G.edgeSet \ {s(v, w)}
Tactic: rw [edgeSet_deleteEdges]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
have rw : ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
Tactic: rw [isBridge_iff, and_congr_right']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
have rw : (¬∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
Tactic: rw [reachable_deleteEdges_iff_exists_walk, not_exists_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
rw : (¬∃ (p : G.Walk v w), s(v, w) ∉ p.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ ¬(G.deleteEdges {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
have rw₁ : (∀ (x : G.Walk v w), s(v, w) ∈ x.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
Tactic: rw [reachable_deleteEdges_iff_exists_walk, not_exists_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
⊢ False
have hv : v ∈ c.support
Tactic: have hv := c.fst_mem_support_of_mem_edges he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
⊢ False
have this : c = (puw.append pwv).append pvu
Tactic: have : c = (puw.append pwv).append pvu := by simp [puw, pwv, pvu]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
⊢ False
have hbq : s(v, w) ∈ (pvu.append puw).edges
Tactic: have hbq := hb (pvu.append puw)