awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h :
  Eq.{u_1 + 1} (α := Sym2 V)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb)
this :
  ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a) (b : V)
    (hb : Membership.mem (γ := Finset V) {default}ᶜ b)
    (h :
      Eq.{u_1 + 1} (α := Sym2 V)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb))
    (h' : (f a).length ≤ (f b).length), a = b
h' : ¬(f a).length ≤ (f b).length
⊢ a = b

Tactic:
Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h :
  Eq.{u_1 + 1} (α := Sym2 V)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb)
this :
  ∀ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a) (b : V)
    (hb : Membership.mem (γ := Finset V) {default}ᶜ b)
    (h :
      Eq.{u_1 + 1} (α := Sym2 V)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb))
    (h' : (f a).length ≤ (f b).length), a = b
h' : ¬(f a).length ≤ (f b).length
⊢ a = b

Tactic:
exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h :
  Eq.{u_1 + 1} (α := Sym2 V)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb)
h' : (f a).length ≤ (f b).length
⊢ (f a).firstDart ⋯ = (f b).firstDart ⋯ ∨ (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm

Tactic:
rw [dart_edge_eq_iff] at h

Premises used: SimpleGraph.dart_edge_eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h :
  Eq.{u_1 + 1} (α := Sym2 V)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha)
    ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) b hb)
h' : (f a).length ≤ (f b).length
h₁ : (f a).firstDart ⋯ = (f b).firstDart ⋯ ∨ (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ (f a).length ≤ (f b).length

Tactic:
rw [dart_edge_eq_iff] at h

Premises used: SimpleGraph.dart_edge_eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h : (f a).firstDart ⋯ = (f b).firstDart ⋯ ∨ (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h' : (f a).length ≤ (f b).length
inl : ∀ (h : (f a).firstDart ⋯ = (f b).firstDart ⋯), a = b
inr : ∀ (h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm), a = b
⊢ a = b

Tactic:
obtain (h | h) := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = (f b).firstDart ⋯
⊢ a = b

Tactic:
(congrArg (·.fst) h)

Premises used: congrArg
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = (f b).firstDart ⋯
⊢ a = b

Tactic:
exact (congrArg (·.fst) h)

Premises used: congrArg
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ a ≠ default

Tactic:
simpa using ha
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ ((f a).firstDart ⋯).toProd.2 = b

Tactic:
have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
inr : ∀ (h3 : ((f a).tail.copy h1 ⋯).length = (f b).length), a = b
inr₁ : ((f a).tail.copy h1 ⋯).IsPath
⊢ a = b

Tactic:
have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).tail.length + 1 = (f b).length + 1
⊢ a ≠ default

Tactic:
simpa using ha
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : ((f a).tail.copy h1 ⋯).length = (f b).length
⊢ (f a).length = (f b).length + 1

Tactic:
rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3

Premises used: SimpleGraph.Walk.length_tail_add_one, add_left_inj, SimpleGraph.Walk.length_copy, SimpleGraph.Walk.not_nil_of_ne, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).length = (f b).length + 1
⊢ a = b

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
inr : (f a).tail.IsPath
⊢ ((f a).tail.copy h1 ⋯).IsPath

Tactic:
simp only [isPath_copy]

Premises used: SimpleGraph.Walk.isPath_copy
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
⊢ (f a).tail.IsPath

Tactic:
(hf _).tail

Premises used: SimpleGraph.Walk.IsPath.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
a : V
ha : Membership.mem (γ := Finset V) {default}ᶜ a
b : V
hb : Membership.mem (γ := Finset V) {default}ᶜ b
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
⊢ (f a).tail.IsPath

Tactic:
exact (hf _).tail

Premises used: SimpleGraph.Walk.IsPath.tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
⊢ ∀ (a₁ : V) (ha₁ : Membership.mem (γ := Finset V) {default}ᶜ a₁) (a₂ : V)
    (ha₂ : Membership.mem (γ := Finset V) {default}ᶜ a₂),
    Eq.{u_1 + 1} (α := Sym2 V)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a₁ ha₁)
        ((fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a₂ ha₂) →
      a₁ = a₂

Tactic:
case inj =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
    rw [dart_edge_eq_iff] at h
    obtain (h | h) := h
    · exact (congrArg (·.fst) h)
    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail

Premises used: SimpleGraph.Walk.length_tail_add_one, SimpleGraph.dart_edge_eq_iff, add_left_inj, SimpleGraph.Walk.isPath_copy, SimpleGraph.Walk.length_copy, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.IsPath.tail, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
simp : ∀ (x y : V), G.Adj x y → ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
⊢ ∀ b ∈ G.edgeFinset,
    ∃ (a : V) (ha : Membership.mem (γ := Finset V) {default}ᶜ a),
      (fun (w : V) (hw : Membership.mem (γ := Finset V) {default}ᶜ w) ↦ ((f w).firstDart ⋯).edge) a ha = b

Tactic:
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]

Premises used: Finset.mem_singleton, Finset.mem_compl, Sym2.forall, SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
inr :
  ∀
    (this :
      ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
        ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y))
    (h' : ¬(f x).length ≤ (f y).length), ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
wlog :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
wlog h' : (f x).length ≤ (f y).length generalizing x y

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
this :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
inr : ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(y, x)
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
this :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(y, x)

Tactic:
this y x h.symm (le_of_not_ge h')

Premises used: SimpleGraph.Adj.symm, le_of_not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this_2 : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
this :
  ∀ (x y : V) (h : G.Adj x y) (h' : (f x).length ≤ (f y).length),
    ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
h' : ¬(f x).length ≤ (f y).length
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(y, x)

Tactic:
exact this y x h.symm (le_of_not_ge h')

Premises used: SimpleGraph.Adj.symm, le_of_not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩

Premises used: Iff.mpr, SimpleGraph.dart_edge_eq_mk'_iff, Exists.intro, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x y : V
h : G.Adj x y
h' : (f x).length ≤ (f y).length
refine_1 : ¬y = default
refine_2 : ((f y).firstDart ⋯).toProd = (y, x)
⊢ ∃ (a : V) (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)

Tactic:
refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : (f x).length ≤ 0
⊢ x ∉ Walk.support (G := G) (u := default) nil

Tactic:
simpa using h.ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : (f x).length ≤ length (u := default) (f default)
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ 0

Tactic:
rw [← hf' _ nil IsPath.nil, length_nil,
          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
          length_cons, length_nil] at h'

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_nil, SimpleGraph.Walk.IsPath.nil, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
hG : G.IsTree
this_1 : Nonempty V
inhabited_h : Inhabited V
this : Finset.card (α := V) {default}ᶜ + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun (p : G.Walk x default) ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun (p : G.Walk x default) ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : HAdd.hAdd (α := ℕ) 0 1 ≤ 0
⊢ False

Tactic:
simp at h'