awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
obtain : ∀ T ≤ G, ∀ (T_isTree : T.IsTree), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
obtain ⟨T, _, T_isTree⟩ := hconn.exists_isTree_le

Premises used: SimpleGraph.Connected.exists_isTree_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
⊢ T.Connected

Tactic:
have ⟨hT, _⟩ := T_isTree
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
⊢ T.IsAcyclic

Tactic:
have ⟨hT, _⟩ := T_isTree
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic : T.IsAcyclic
have : ∀ (this : Fintype V), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
have := Fintype.ofFinite V
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic : T.IsAcyclic
this : Fintype V
obtain : ∀ (v : V) (hv : T.degree v = 1), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial

Premises used: SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic : T.IsAcyclic
this : Fintype V
v : V
hv : T.degree v = 1
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ ⦃v_1 w : (↑{v}ᶜ : Type u_1)⦄, Adj (induce {v}ᶜ T) v_1 w → Adj (induce {v}ᶜ G) v_1 w
⊢ LE.le (α := SimpleGraph (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ T) (induce {v}ᶜ G)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic : T.IsAcyclic
this : Fintype V
v : V
hv : T.degree v = 1
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic : T.IsAcyclic
this : Fintype V
obtain : ∀ (v : V) (hv : T.degree v = 1), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
classical
  obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial
  exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
⊢ Nontrivial V

Tactic:
nontriviality V using hconn.nonempty

Premises used: SimpleGraph.Connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
h : Nontrivial V
obtain :
  ∀ (v : V) (hv : Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)),
    ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
obtain ⟨v, hv⟩ := hconn.exists_connected_induce_compl_singleton_of_finite_nontrivial

Premises used: SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
h : Nontrivial V
v : V
hv : Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
⟨v, hv.preconnected⟩

Premises used: SimpleGraph.Connected.preconnected, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
h : Nontrivial V
v : V
hv : Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
exact ⟨v, hv.preconnected⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
obtain : ∀ (p : G.Walk u v) (hp : p.IsPath) (hp' : p.length = G.dist u v), G.dist u v ≠ G.dist u w
⊢ G.dist u v ≠ G.dist u w

Tactic:
obtain ⟨p, hp, hp'⟩ := hreach.exists_path_of_dist

Premises used: SimpleGraph.Reachable.exists_path_of_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
obtain : ∀ (q : G.Walk u w) (hq : q.IsPath) (hq' : q.length = G.dist u w), G.dist u v ≠ G.dist u w
⊢ G.dist u v ≠ G.dist u w

Tactic:
obtain ⟨q, hq, hq'⟩ := hreach.trans hadj.reachable |>.exists_path_of_dist

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.Reachable.trans, SimpleGraph.Reachable.exists_path_of_dist
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
rw : p.length ≠ q.length
⊢ G.dist u v ≠ G.dist u w

Tactic:
rw [← hp', ← hq']
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
pos : ∀ (hw : w ∈ p.support), p.length ≠ q.length
neg : ∀ (hw : w ∉ p.support), p.length ≠ q.length
⊢ p.length ≠ q.length

Tactic:
by_cases hw : w ∈ p.support

Premises used: SimpleGraph.Walk.support
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
pos : q.length + 1 ≠ q.length
⊢ p.length ≠ q.length

Tactic:
rw [hG.path_concat hq hp hadj.symm hw, q.length_concat]

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Walk.length_concat, SimpleGraph.IsAcyclic.path_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
⊢ q.length + 1 ≠ q.length

Tactic:
q.length.ne_add_one.symm

Premises used: SimpleGraph.Walk.length, Ne.symm, Nat.ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∈ p.support
⊢ q.length + 1 ≠ q.length

Tactic:
exact q.length.ne_add_one.symm

Premises used: SimpleGraph.Walk.length, Ne.symm, Nat.ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
⊢ v ∈ q.support

Tactic:
have hv : v ∈ q.support := hG.mem_support_of_ne_mem_support_of_adj_of_isPath hq hp
      hadj.symm hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
neg : p.length ≠ p.length + 1
⊢ p.length ≠ q.length

Tactic:
rw [hG.path_concat hp hq hadj hv, p.length_concat]

Premises used: SimpleGraph.Walk.length_concat, SimpleGraph.IsAcyclic.path_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1

Tactic:
p.length.ne_add_one

Premises used: SimpleGraph.Walk.length, Nat.ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1

Tactic:
exact p.length.ne_add_one

Premises used: SimpleGraph.Walk.length, Nat.ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
u v w : V
hadj : G.Adj v w
⊢ G.dist u v ≠ G.dist u w

Tactic:
hG.isAcyclic.dist_ne_of_adj hadj <| hG.connected u v

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.IsAcyclic.dist_ne_of_adj, SimpleGraph.IsTree.connected, SimpleGraph.IsTree.isAcyclic
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
grind [dist_ne_of_adj, Adj.diff_dist_adj]

Premises used: SimpleGraph.IsAcyclic.dist_ne_of_adj, SimpleGraph.Adj.diff_dist_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
u v w : V
hadj : G.Adj v w
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
grind [dist_ne_of_adj, Adj.diff_dist_adj]

Premises used: SimpleGraph.IsTree.dist_ne_of_adj, SimpleGraph.Adj.diff_dist_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsTree
u : V
⊢ ∀ {v w : V},
    G.Adj v w →
      Ne (α := Fin 2) ((fun (v : V) ↦ (⟨G.dist u v % 2, ⋯⟩ : Fin 2)) v)
        ((fun (v : V) ↦ (⟨G.dist u v % 2, ⋯⟩ : Fin 2)) w)

Tactic:
grind [dist_eq_dist_add_one_of_adj]

Premises used: SimpleGraph.IsTree.dist_eq_dist_add_one_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
⊢ G.IsBipartite

Tactic:
⟨hG.coloringTwo⟩

Premises used: SimpleGraph.IsTree.coloringTwo, Nonempty.intro, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
hadj : G.Adj u v
⊢ G.connectedComponentMk u = G.connectedComponentMk v

Tactic:
have := ConnectedComponent.sound hadj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
hadj : G.Adj u v
this : G.connectedComponentMk u = G.connectedComponentMk v
⊢ G.dist (verts (G.connectedComponentMk u)) u = G.dist (verts (G.connectedComponentMk u)) v + 1 ∨
    G.dist (verts (G.connectedComponentMk u)) v = G.dist (verts (G.connectedComponentMk u)) u + 1

Tactic:
have := hG.dist_eq_dist_add_one_of_adj_of_reachable _ hadj <| ConnectedComponent.exact <| h _
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
u v : V
hadj : G.Adj u v
this_1 : G.connectedComponentMk u = G.connectedComponentMk v
this :
  G.dist (verts (G.connectedComponentMk u)) u = G.dist (verts (G.connectedComponentMk u)) v + 1 ∨
    G.dist (verts (G.connectedComponentMk u)) v = G.dist (verts (G.connectedComponentMk u)) u + 1
⊢ Adj (V := Fin 2) (completeGraph (Fin 2))
    (let u_1 := verts (G.connectedComponentMk u);
    ⟨G.dist u_1 u % 2, ⋯⟩)
    (let u := verts (G.connectedComponentMk v);
    ⟨G.dist u v % 2, ⋯⟩)

Tactic:
grind [top_adj]

Premises used: SimpleGraph.top_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
⊢ G.IsBipartite

Tactic:
⟨hG.coloringTwo⟩

Premises used: Nonempty.intro, SimpleGraph.IsAcyclic.coloringTwo, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
⊢ G.Colorable 2

Tactic:
hG.isBipartite

Premises used: SimpleGraph.IsAcyclic.isBipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
⊢ G.Colorable 2

Tactic:
hG.isAcyclic.colorable_two

Premises used: SimpleGraph.IsAcyclic.colorable_two, SimpleGraph.IsTree.isAcyclic
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
⊢ G.chromaticNumber ≤ 2

Tactic:
hG.colorable_two.chromaticNumber_le

Premises used: SimpleGraph.IsAcyclic.colorable_two, SimpleGraph.Colorable.chromaticNumber_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
hG : G.IsTree
⊢ G.chromaticNumber ≤ 2

Tactic:
hG.colorable_two.chromaticNumber_le

Premises used: SimpleGraph.Colorable.chromaticNumber_le, SimpleGraph.IsTree.colorable_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h : G.IsEdgeReachable n u v
obtain : ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w), ∃ (w : G.Walk u u), w.IsCycle
⊢ ∃ (w : G.Walk u u), w.IsCycle

Tactic:
obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn)

Premises used: SimpleGraph.exists_adj_isEdgeReachable_two, SimpleGraph.IsEdgeReachable.anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
simp : LT.lt (α := ℕ∞) 1 2
⊢ Set.encard (α := Sym2 V) {s(u, w)} < (↑2 : ℕ∞)

Tactic:
simp only [Set.encard_singleton, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Set.encard_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
⊢ LT.lt (α := ℕ∞) 1 2

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
⊢ (G.deleteEdges {s(u, w)}).Reachable u w

Tactic:
have := @h {s(u, w)} (by simp only [Set.encard_singleton, Nat.cast_ofNat]; decide)
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
this : (G.deleteEdges {s(u, w)}).Reachable u w
obtain : ∀ (w_1 : V) (p : G.Walk w_1 w_1) (hp₁ : p.IsCycle) (hp₂ : s(u, w) ∈ p.edges), ∃ (w : G.Walk u u), w.IsCycle
⊢ ∃ (w : G.Walk u u), w.IsCycle

Tactic:
obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩

Premises used: SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w_1 : V
hw : G.Adj u w_1
h : G.IsEdgeReachable 2 u w_1
this : (G.deleteEdges {s(u, w_1)}).Reachable u w_1
w : V
p : G.Walk w w
hp₁ : p.IsCycle
hp₂ : s(u, w_1) ∈ p.edges
⊢ ∃ (w : G.Walk u u), w.IsCycle

Tactic:
⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩

Premises used: SimpleGraph.Walk.rotate, Exists.intro, SimpleGraph.Walk.IsCycle.rotate, SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h_1 : G.IsEdgeReachable n u v
w_1 : V
hw : G.Adj u w_1
h : G.IsEdgeReachable 2 u w_1
this : (G.deleteEdges {s(u, w_1)}).Reachable u w_1
w : V
p : G.Walk w w
hp₁ : p.IsCycle
hp₂ : s(u, w_1) ∈ p.edges
⊢ ∃ (w : G.Walk u u), w.IsCycle

Tactic:
exact ⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h : G.IsEdgeReachable n u v
obtain obtain₁ : ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w), ∃ (w : G.Walk u u), w.IsCycle
obtain₂ :
  ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w) (this : (G.deleteEdges {s(u, w)}).Reachable u w),
    ∃ (w : G.Walk u u), w.IsCycle
obtain₃ :
  ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w) (this : (G.deleteEdges {s(u, w)}).Reachable u w) (w_1 : V)
    (p : G.Walk w_1 w_1) (hp₁ : p.IsCycle) (hp₂ : s(u, w) ∈ p.edges), ∃ (w : G.Walk u u), w.IsCycle
⊢ ∃ (w : G.Walk u u), w.IsCycle

Tactic:
classical
  obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn)
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), this was just
  `have := @h {s(u, w)} (by simp)`. It is not yet clear whether this is due to defeq abuse in
  Mathlib or a problem in the new canonicalizer; a minimization would help. -/
  have := @h {s(u, w)} (by simp only [Set.encard_singleton, Nat.cast_ofNat]; decide)
  obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩
  exact ⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩

Premises used: SimpleGraph.exists_adj_isEdgeReachable_two, SimpleGraph.IsEdgeReachable.anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2

Tactic:
⟨fun h _ _ hne he ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
refine_1 : ∀ (h : G.IsAcyclic) (x x_1 : V) (hne : x ≠ x_1) (he : G.IsEdgeReachable 2 x x_1), False
refine_2 : ∀ (h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2), G.IsAcyclic
⊢ G.IsAcyclic ↔ Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2

Tactic:
refine ⟨fun h _ _ hne he ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
x x_1 : V
hne : x ≠ x_1
he : G.IsEdgeReachable 2 x x_1
refine_1 : ∀ (w : G.Walk x x) (hw : w.IsCycle), False
⊢ False

Tactic:
obtain ⟨w, hw⟩ := exists_isCycle_of_two_le_isEdgeReachable hne le_rfl he

Premises used: le_rfl, SimpleGraph.exists_isCycle_of_two_le_isEdgeReachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
x x_1 : V
hne : x ≠ x_1
he : G.IsEdgeReachable 2 x x_1
w : G.Walk x x
hw : w.IsCycle
⊢ False

Tactic:
h w hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
x x_1 : V
hne : x ≠ x_1
he : G.IsEdgeReachable 2 x x_1
w : G.Walk x x
hw : w.IsCycle
⊢ False

Tactic:
exact h w hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ G.IsAcyclic

Tactic:
isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ hadj ↦ ?_

Premises used: Iff.mpr, SimpleGraph.isAcyclic_iff_forall_adj_isBridge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
refine_2 : ∀ (x x_1 : V) (hadj : G.Adj x x_1), G.IsBridge s(x, x_1)
⊢ G.IsAcyclic

Tactic:
refine isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ hadj ↦ ?_

Premises used: Iff.mpr, SimpleGraph.isAcyclic_iff_forall_adj_isBridge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
x x_1 : V
hadj : G.Adj x x_1
⊢ G.IsBridge s(x, x_1)

Tactic:
isBridge_iff_adj_and_not_isEdgeConnected_two.mpr ⟨hadj, h hadj.ne⟩

Premises used: Iff.mpr, SimpleGraph.Adj.ne, And.intro, SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
x x_1 : V
hadj : G.Adj x x_1
⊢ G.IsBridge s(x, x_1)

Tactic:
exact isBridge_iff_adj_and_not_isEdgeConnected_two.mpr ⟨hadj, h hadj.ne⟩

Premises used: Iff.mpr, SimpleGraph.Adj.ne, And.intro, SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i : V
⊢ ¬A i i = 1

Tactic:
simp [h.apply_diag i]

Premises used: Matrix.IsAdjMatrix.apply_diag
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i j : V
inl : ∀ (h : A i j = 0), ¬A i j = 1 ↔ A i j = 0
inr : ∀ (h : A i j = 1), ¬A i j = 1 ↔ A i j = 0
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
obtain h | h := h.zero_or_one i j

Premises used: Matrix.IsAdjMatrix.zero_or_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h_1 : A.IsAdjMatrix
i j : V
h : A i j = 0
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h_1 : A.IsAdjMatrix
i j : V
h : A i j = 1
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i j : V
rw : ¬¬A i j = 1 ↔ A i j = 1
rw₁ rw₂ : A i j = 1 ↔ A i j = 1
⊢ ¬A i j = 0 ↔ A i j = 1

Tactic:
rw [← apply_ne_one_iff h, Classical.not_not]

Premises used: Matrix.IsAdjMatrix.apply_ne_one_iff, Classical.not_not
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i j : V
hij : (fun (i j : V) ↦ A i j = 1) i j
rwa rwa₁ rwa₂ rwa₃ : A i j = 1
⊢ A j i = 1

Tactic:
rwa [h.symm.apply i j]

Premises used: Matrix.IsAdjMatrix.symm, Matrix.IsSymm.apply
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i : V
⊢ ¬A i i = 1

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
inst_2 : DecidableEq α
h : A.IsAdjMatrix
⊢ DecidableRel fun (i j : V) ↦ A i j = 1

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
a : ∀ (i j : V), (A ⊙ A) i j = A i j
⊢ A ⊙ A = A

Tactic:
ext i j