awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h_1 : 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)
rw : (G.deleteEdges {s(x, y)}).edgeFinset.card < G.edgeFinset.card
⊢ Nat.card.{u_1} (↑(G.deleteEdges {s(x, y)}).edgeSet : Type u_1) + 1 < Nat.card V

Tactic:
rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]

Premises used: add_lt_add_iff_right, SimpleGraph.edgeFinset_card, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h_1 : 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 ⊂ G.edgeFinset

Tactic:
simpa [deleteEdges, edgeFinset]

Premises used: SimpleGraph.deleteEdges, SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
this : Fintype V
h_1 : 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:
exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]

Premises used: Finset.card_lt_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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
⊢ G.IsTree ↔ G.Connected ∧ Nat.card.{u_1} (↑G.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]

Premises used: SimpleGraph.isAcyclic_iff_forall_adj_isBridge, Finset.card_lt_card, add_lt_add_iff_right, SimpleGraph.edgeFinset_card, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
neg : ∀ (q : ¬2 ≤ G.minDegree), G.minDegree = 1
⊢ G.minDegree = 1

Tactic:
by_cases q : 2 ≤ G.minDegree

Premises used: SimpleGraph.minDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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.edgeFinset.card + 1 = Fintype.card V

Tactic:
have := h.card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ ∑ v : V, G.degree v = 2 * G.edgeFinset.card

Tactic:
have := G.sum_degrees_eq_twice_card_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
h₁ : ∀ (i : V), Membership.mem (γ := Finset V) Finset.univ i → 2 ≤ G.degree i
⊢ LE.le (α := ℕ) (∑ v : V, 2) (∑ v : V, G.degree v)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
i : V
h_1 : Membership.mem (γ := Finset V) Finset.univ i
⊢ 2 ≤ G.degree i

Tactic:
le_trans q (G.minDegree_le_degree _)

Premises used: SimpleGraph.minDegree_le_degree, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
i : V
h_1 : Membership.mem (γ := Finset V) Finset.univ i
⊢ 2 ≤ G.degree i

Tactic:
exact le_trans q (G.minDegree_le_degree _)

Premises used: SimpleGraph.minDegree_le_degree, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)

Tactic:
have hle : ∑ v : V, 2 ≤ ∑ v, G.degree v := by
      gcongr
      exact le_trans q (G.minDegree_le_degree _)
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)
⊢ Fintype.card V * 2 ≤ ∑ v : V, G.degree v

Tactic:
rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle

Premises used: Finset.card_univ, smul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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 : Fintype.card V * 2 ≤ ∑ v : V, G.degree v
⊢ G.minDegree = 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ 0 < G.minDegree

Tactic:
have := h.preconnected.minDegree_pos_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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 : 0 < G.minDegree
⊢ G.minDegree = 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Nontrivial V
inst_2 : DecidableRel G.Adj
h : G.IsTree
obtain : ∀ (v : V) (hv : G.minDegree = G.degree v), ∃ (v : V), G.degree v = 1
⊢ ∃ (v : V), G.degree v = 1

Tactic:
obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex

Premises used: SimpleGraph.exists_minimal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
h₁ : G.degree v = 1
⊢ ∃ (v : V), G.degree v = 1

Tactic:
use v
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
h₁ : G.minDegree = 1
⊢ G.degree v = 1

Tactic:
rw [← hv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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.minDegree = 1

Tactic:
h.minDegree_eq_one_of_nontrivial

Premises used: SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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.minDegree = 1

Tactic:
exact h.minDegree_eq_one_of_nontrivial

Premises used: SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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)
⊢ Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
obtain ⟨u, adj_vu, hu⟩ := degree_eq_one_iff_existsUnique_adj.mp hdeg

Premises used: Iff.mp, SimpleGraph.degree_eq_one_iff_existsUnique_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ Membership.mem (γ := Set V) {v}ᶜ u

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
refine : Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
refine (connected_iff _).mpr ⟨?_, u, by aesop⟩

Premises used: Iff.mpr, Nonempty.intro, And.intro, SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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)
obtain : ∀ (pwu : G.Walk (↑w : V) u) (hpwu : pwu.IsPath), Reachable (induce {v}ᶜ G) w x
⊢ Reachable (induce {v}ᶜ G) w x

Tactic:
obtain ⟨pwu, hpwu⟩ := hconn.exists_isPath w u

Premises used: SimpleGraph.Connected.exists_isPath, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
obtain : ∀ (pux : G.Walk u (↑x : V)) (hpux : pux.IsPath), Reachable (induce {v}ᶜ G) w x
⊢ Reachable (induce {v}ᶜ G) w x

Tactic:
obtain ⟨pux, hpux⟩ := hconn.exists_isPath u x

Premises used: SimpleGraph.Connected.exists_isPath, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
rw : ∃ (x : Walk (induce {v}ᶜ G) w x), True
⊢ Reachable (induce {v}ᶜ G) w x

Tactic:
rw [Reachable, ← exists_true_iff_nonempty]

Premises used: exists_true_iff_nonempty, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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₁ : ∀ x_1 ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support, Membership.mem (γ := Set V) {v}ᶜ x_1
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True

Tactic:
use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)

Premises used: SetCoe.ext, SimpleGraph.Walk.induce, Compl.compl, SimpleGraph.Walk.toPath, SimpleGraph.Walk.copy, Singleton.singleton, Subtype.val, rfl, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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
⊢ ¬z = v

Tactic:
obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz

Premises used: SimpleGraph.Walk.mem_support_iff_exists_append, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
w₁ : ∀ (this : z = v), False
⊢ ¬z = v

Tactic:
by_contra
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
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
⊢ False

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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

Tactic:
List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_

Premises used: List.nodup_iff_forall_not_duplicate, SimpleGraph.Walk.toPath, SimpleGraph.Path.nodup_support, Iff.mp, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
w₁ : List.Duplicate u (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support
⊢ False

Tactic:
refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_

Premises used: List.nodup_iff_forall_not_duplicate, SimpleGraph.Walk.toPath, SimpleGraph.Path.nodup_support, Iff.mp, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
w₁ : 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
⊢ List.Duplicate u (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support

Tactic:
rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]

Premises used: List.count_append, SimpleGraph.Walk.support_append, List.duplicate_iff_two_le_count
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ 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))
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ (↑w : V) ≠ z

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ 1 ≤ List.count u pwz.support

Tactic:
simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this

Premises used: SimpleGraph.Walk.adj_penultimate, SimpleGraph.Adj.symm, SimpleGraph.Walk.not_nil_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ z ≠ (↑x : V)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ 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)))
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ z ≠ (↑x : V)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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
⊢ 1 ≤ List.count u pzx.support.tail

Tactic:
rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this

Premises used: SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
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 u pzx.support.tail
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail

Tactic:
lia