awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
refine :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V), G.IsAcyclic
refine₁ :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) ⦃v w : V⦄,
      G.Adj v w → G.IsBridge s(v, w)
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have refine₂ : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
  ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) (x y : V) (h : G.Adj x y)
    (hbr : ¬G.IsBridge s(x, y)), Nat.card.{u_1} (↑(G.deleteEdges {s(x, y)}).edgeSet : Type u_1) + 1 < Nat.card V
Tactic: classical
  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
  rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
refine :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V), G.IsAcyclic
refine₁ :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) ⦃v w : V⦄,
      G.Adj v w → G.IsBridge s(v, w)
refine₂ :
  G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
    ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) (x y : V) (h : G.Adj x y)
      (hbr : ¬G.IsBridge s(x, y)), Nat.card.{u_1} (↑(G.deleteEdges {s(x, y)}).edgeSet : Type u_1) + 1 < Nat.card V
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V
have refine₃ : G.Connected ∧ Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V →
  ∀ (h₁ : G.Connected) (h₂ : Nat.card.{u_1} (↑G.edgeSet : Type u_1) + 1 = Nat.card V) (x y : V) (h : G.Adj x y)
    (hbr : ¬G.IsBridge s(x, y)), (G.deleteEdges {s(x, y)}).edgeFinset.card < G.edgeFinset.card
Tactic: classical
  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦
    (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
  rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]
  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
⊢ G.minDegree = 1
have pos : ∀ (q : 2 ≤ G.minDegree), G.minDegree = 1
Tactic: by_cases q : 2 ≤ G.minDegree
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
pos : ∀ (q : 2 ≤ G.minDegree), G.minDegree = 1
⊢ G.minDegree = 1
have neg : ∀ (q : ¬2 ≤ G.minDegree), G.minDegree = 1
Tactic: by_cases q : 2 ≤ G.minDegree
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : 2 ≤ G.minDegree
⊢ G.minDegree = 1
have this : G.edgeFinset.card + 1 = Fintype.card V
Tactic: have := h.card_edgeFinset
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this : G.edgeFinset.card + 1 = Fintype.card V
⊢ G.minDegree = 1
have this₁ : ∑ v : V, G.degree v = 2 * G.edgeFinset.card
Tactic: have := G.sum_degrees_eq_twice_card_edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this_1 : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v : V, G.degree v = 2 * G.edgeFinset.card
⊢ LE.le (α := ℕ) (∑ v : V, 2) (∑ v : V, G.degree v)
have h₁ : ∀ (i : V), Membership.mem (γ := Finset V) Finset.univ i → 2 ≤ G.degree i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this_1 : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v : V, G.degree v = 2 * G.edgeFinset.card
⊢ G.minDegree = 1
have hle : LE.le (α := ℕ) (∑ v : V, 2) (∑ v : V, G.degree v)
Tactic: have hle : ∑ v : V, 2 ≤ ∑ v, G.degree v := by
      gcongr
      exact le_trans q (G.minDegree_le_degree _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this_1 : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v : V, G.degree v = 2 * G.edgeFinset.card
hle : LE.le (α := ℕ) (∑ v : V, 2) (∑ v : V, G.degree v)
⊢ G.minDegree = 1
have hle₁ : Fintype.card V * 2 ≤ ∑ v : V, G.degree v
Tactic: rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
q : ¬2 ≤ G.minDegree
⊢ G.minDegree = 1
have this : 0 < G.minDegree
Tactic: have := h.preconnected.minDegree_pos_of_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
h : G.IsTree
⊢ ∃ (v : V), G.degree v = 1
have obtain : ∀ (v : V) (hv : G.minDegree = G.degree v), ∃ (v : V), G.degree v = 1
Tactic: obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
h : G.IsTree
v : V
hv : G.minDegree = G.degree v
⊢ ∃ (v : V), G.degree v = 1
have h₁ : G.degree v = 1
Tactic: use v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
h : G.IsTree
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v = 1
have h₁ : G.minDegree = 1
Tactic: rw [← hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
⊢ Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have obtain : ∀ (u : V) (adj_vu : G.Adj v u) (hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u),
  Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: obtain ⟨u, adj_vu, hu⟩ := degree_eq_one_iff_existsUnique_adj.mp hdeg
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
⊢ Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have refine : Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: refine (connected_iff _).mpr ⟨?_, u, by aesop⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
⊢ Reachable (induce {v}ᶜ G) w x
have obtain : ∀ (pwu : G.Walk (↑w : V) u) (hpwu : pwu.IsPath), Reachable (induce {v}ᶜ G) w x
Tactic: obtain ⟨pwu, hpwu⟩ := hconn.exists_isPath w u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
⊢ Reachable (induce {v}ᶜ G) w x
have obtain : ∀ (pux : G.Walk u (↑x : V)) (hpux : pux.IsPath), Reachable (induce {v}ᶜ G) w x
Tactic: obtain ⟨pux, hpux⟩ := hconn.exists_isPath u x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
⊢ Reachable (induce {v}ᶜ G) w x
have rw : ∃ (x : Walk (induce {v}ᶜ G) w x), True
Tactic: rw [Reachable, ← exists_true_iff_nonempty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have w₁ : ∀ x_1 ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support, Membership.mem (γ := Set V) {v}ᶜ x_1
Tactic: use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
⊢ ¬z = v
have w₁ : ∀ (pwz : G.Walk (↑w : V) z) (pzx : G.Walk z (↑x : V))
  (p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx), ¬z = v
Tactic: obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
this : z = v
⊢ False
have w₁ : ∀ [inst : Fintype (↑(G.neighborSet z) : Type u_1)] (hdeg : G.degree z = 1) (adj_vu : G.Adj z u)
  (hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u) (w x : (↑{z}ᶜ : Type u_1)) (pwu : G.Walk (↑w : V) u)
  (hpwu : pwu.IsPath) (pux : G.Walk u (↑x : V)) (hpux : pux.IsPath)
  (hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support) (pwz : G.Walk (↑w : V) z)
  (pzx : G.Walk z (↑x : V)) (p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx), False
Tactic: subst_vars
Cleared hypotheses: v, inst, hdeg, adj_vu, hu, w, x, pwu, hpwu, pux, hpux, hz, pwz, pzx, p_eq_pwzx, this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
⊢ False
have w₁ : List.Duplicate u (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
Tactic: refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
⊢ List.Duplicate u (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
have w₁ : 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
Tactic: rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
have this : 1 ≤ List.count (pwz.getVert (pwz.length - 1)) pwz.support
Tactic: have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
this : 1 ≤ List.count (pwz.getVert (pwz.length - 1)) pwz.support
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
have this₁ : 1 ≤ List.count u pwz.support
Tactic: simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
this : 1 ≤ List.count u pwz.support
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
have this₁ : 1 ≤ List.count pzx.snd pzx.support.tail
Tactic: have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst : Fintype (↑(G.neighborSet z) : Type u_1)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj z w) y → y = u
w x : (↑{z}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
pwz : G.Walk (↑w : V) z
pzx : G.Walk z (↑x : V)
p_eq_pwzx : (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)) = pwz.append pzx
this_1 : 1 ≤ List.count u pwz.support
this : 1 ≤ List.count pzx.snd pzx.support.tail
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
have this₁ : 1 ≤ List.count u pzx.support.tail
Tactic: rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have w₁ : Walk (induce {v}ᶜ G) w x
Tactic: classical
  use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
w₁ : Walk (induce {v}ᶜ G) w x
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have h : True
Tactic: classical
  use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
w₁ : Walk (induce {v}ᶜ G) w x
h : True
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have w₂ : ∀ x_1 ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support, Membership.mem (γ := Set V) {v}ᶜ x_1
Tactic: classical
  use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun (w : V) ↦ G.Adj v w) y → y = u
w x : (↑{v}ᶜ : Type u_1)
pwu : G.Walk (↑w : V) u
hpwu : pwu.IsPath
pux : G.Walk u (↑x : V)
hpux : pux.IsPath
w₁ : Walk (induce {v}ᶜ G) w x
h : True
w₂ w₃ :
  ∀ (z : V) (hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support), Membership.mem (γ := Set V) {v}ᶜ z
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have w₄ : ∀ (z : V) (hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support), ¬z = v
Tactic: classical
  use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia