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
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
w₄ : ∀ (z : V) (hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support), ¬z = v
⊢ ∃ (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) (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: 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
w₄ : ∀ (z : V) (hz : z ∈ (↑(pwu.append pux).toPath : G.Walk (↑w : V) (↑x : V)).support), ¬z = v
w₅ :
  ∀ (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),
    ¬z = v
w₆ :
  ∀ (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
⊢ ∃ (x : Walk (induce {v}ᶜ G) w x), True
have w₇ : ∀ (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: 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
Cleared hypotheses: v, inst, hdeg, adj_vu, hu, w, x, pwu, hpwu, pux, hpux
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
inst_1 : Nontrivial V
hconn : G.Connected
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have obtain : ∀ T ≤ G, ∀ (T_isTree : T.IsTree), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: obtain ⟨T, _, T_isTree⟩ := hconn.exists_isTree_le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have hT : T.Connected
Tactic: have ⟨hT, _⟩ := T_isTree
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have isAcyclic : T.IsAcyclic
Tactic: have ⟨hT, _⟩ := T_isTree
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have have : ∀ (this : Fintype V), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: have := Fintype.ofFinite V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have obtain : ∀ (v : V) (hv : T.degree v = 1), ∃ (v : V), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ LE.le (α := SimpleGraph (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ T) (induce {v}ᶜ G)
have tauto : ∀ ⦃v_1 w : (↑{v}ᶜ : Type u_1)⦄, Adj (induce {v}ᶜ T) v_1 w → Adj (induce {v}ᶜ G) v_1 w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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), Connected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have obtain : ∀ (v : V) (hv : T.degree v = 1), ∃ (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)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
⊢ ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have a : Nontrivial V
Tactic: nontriviality V using hconn.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hconn : G.Connected
h : Nontrivial V
⊢ ∃ (v : V), Preconnected (V := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have obtain : ∀ (v : V) (hv : Connected (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
have obtain : ∀ (p : G.Walk u v) (hp : p.IsPath) (hp' : p.length = G.dist u v), G.dist u v ≠ G.dist u w
Tactic: obtain ⟨p, hp, hp'⟩ := hreach.exists_path_of_dist
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.dist u v ≠ G.dist u w
have obtain : ∀ (q : G.Walk u w) (hq : q.IsPath) (hq' : q.length = 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.dist u v ≠ G.dist u w
have rw : p.length ≠ q.length
Tactic: rw [← hp', ← hq']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p.length ≠ q.length
have pos : ∀ (hw : w ∈ p.support), p.length ≠ q.length
Tactic: by_cases hw : w ∈ p.support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p.length ≠ q.length
have neg : ∀ (hw : w ∉ p.support), p.length ≠ q.length
Tactic: by_cases hw : w ∈ p.support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ p.length ≠ q.length
have pos : q.length + 1 ≠ q.length
Tactic: rw [hG.path_concat hq hp hadj.symm hw, q.length_concat]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ p.length ≠ q.length
have hv : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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 ≠ q.length
have neg : p.length ≠ p.length + 1
Tactic: rw [hG.path_concat hp hq hadj hv, p.length_concat]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ 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, ⋯⟩)
have this : G.connectedComponentMk u = G.connectedComponentMk v
Tactic: have := ConnectedComponent.sound hadj.reachable
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ 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, ⋯⟩)
have 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
Tactic: have := hG.dist_eq_dist_add_one_of_adj_of_reachable _ hadj <| ConnectedComponent.exact <| h _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h : G.IsEdgeReachable n u v
⊢ ∃ (w : G.Walk u u), w.IsCycle
have obtain : ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w), ∃ (w : G.Walk u u), w.IsCycle
Tactic: obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ Set.encard (α := Sym2 V) {s(u, w)} < (↑2 : ℕ∞)
have simp : LT.lt (α := ℕ∞) 1 2
Tactic: simp only [Set.encard_singleton, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (hypothesis)
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
⊢ ∃ (w : G.Walk u u), w.IsCycle
have this : (G.deleteEdges {s(u, w)}).Reachable u w
Tactic: have := @h {s(u, w)} (by simp only [Set.encard_singleton, Nat.cast_ofNat]; decide)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ ∃ (w : G.Walk u u), w.IsCycle
have 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
Tactic: obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h : G.IsEdgeReachable n u v
⊢ ∃ (w : G.Walk u u), w.IsCycle
have obtain : ∀ (w : V) (hw : G.Adj u w) (h : G.IsEdgeReachable 2 u w), ∃ (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 _⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ ∃ (w : G.Walk u u), w.IsCycle
have 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
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 _⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ ∃ (w : G.Walk u u), w.IsCycle
have 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
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 _⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
have refine_1 : ∀ (h : G.IsAcyclic) (x x_1 : V) (hne : x ≠ x_1) (he : G.IsEdgeReachable 2 x x_1), False
Tactic: refine ⟨fun h _ _ hne he ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ G.IsAcyclic ↔ Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
have refine_2 : ∀ (h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2), G.IsAcyclic
Tactic: refine ⟨fun h _ _ hne he ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
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
⊢ False
have refine_1 : ∀ (w : G.Walk x x) (hw : w.IsCycle), False
Tactic: obtain ⟨w, hw⟩ := exists_isCycle_of_two_le_isEdgeReachable hne le_rfl he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Acyclic (goal)
Goal:
V : Type u_1
G : SimpleGraph V
h : Pairwise fun (x1 x2 : V) ↦ ¬G.IsEdgeReachable 2 x1 x2
⊢ G.IsAcyclic
have refine_2 : ∀ (x x_1 : V) (hadj : G.Adj x x_1), G.IsBridge s(x, x_1)
Tactic: refine isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ hadj ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0
have inl : ∀ (h : A i j = 0), ¬A i j = 1 ↔ A i j = 0
Tactic: obtain h | h := h.zero_or_one i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
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
⊢ ¬A i j = 1 ↔ A i j = 0
have inr : ∀ (h : A i j = 1), ¬A i j = 1 ↔ A i j = 0
Tactic: obtain h | h := h.zero_or_one i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst : MulZeroOneClass α
inst_1 : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 0 ↔ A i j = 1
have rw : ¬¬A i j = 1 ↔ A i j = 1
Tactic: rw [← apply_ne_one_iff h, Classical.not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
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
⊢ ¬A i j = 0 ↔ A i j = 1
have rw₁ : A i j = 1 ↔ A i j = 1
Tactic: rw [← apply_ne_one_iff h, Classical.not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A ⊙ A = A
have a : ∀ (i j : V), (A ⊙ A) i j = A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (hypothesis)
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ (A ⊙ A) i j = A i j
have this : A i j = 0 ∨ A i j = 1
Tactic: have := hA.zero_or_one i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : MonoidWithZero α
inst_2 : IsLeftCancelMulZero α
A : Matrix V V α
⊢ A.IsAdjMatrix ↔ A ⊙ A = A ∧ A.IsSymm ∧ 1 ⊙ A = 0
have simp : A.IsAdjMatrix ↔ (∀ (i j : V), A i j = 0 ∨ A i j = 1) ∧ A.IsSymm ∧ ∀ (x : V), A x x = 0
Tactic: simp only [hadamard_self_eq_self_iff, IsIdempotentElem.iff_eq_zero_or_one,
    one_hadamard_eq_zero_iff, funext_iff, diag, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1
have simp : (¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0) ∨
  Eq.{u_1 + 1} (α := α) (if i = j then 0 else if A i j = 0 then 1 else 0) 1
Tactic: simp [compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
h : A.IsSymm
⊢ A.compl.IsSymm
have a : ∀ (i j : V), A.complᵀ i j = A.compl i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (hypothesis)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
h : A.compl = B.compl
i j : V
⊢ A i j = B i j
have h₁ : Eq (α := V → V → α) (fun (i j : V) ↦ if i = j then 0 else if A i j = 0 then 1 else 0) fun (i j : V) ↦
  if i = j then 0 else if B i j = 0 then 1 else 0
Tactic: simp [compl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A.compl.compl = A
have a : ∀ (i j : V), A.compl.compl i j = A i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.AdjMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ A.compl.compl i j = A i j
have a : (if i = j then 0 else if ¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0 then 1 else 0) = A i j
Tactic: simp [compl]