awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
subst_vars : ∀ (e : u' ⟶ v'), cast ⋯ ⋯ e ≍ e
⊢ cast hu hv e ≍ e

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u' v' : U
e : u' ⟶ v'
⊢ cast ⋯ ⋯ e ≍ e

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
rw : _root_.cast ⋯ e = e' ↔ e ≍ e'
⊢ cast hu hv e = e' ↔ e ≍ e'

Tactic:
rw [Hom.cast_eq_cast]

Premises used: Quiver.Hom.cast_eq_cast
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast ⋯ e = e' ↔ e ≍ e'

Tactic:
_root_.cast_eq_iff_heq

Premises used: cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast ⋯ e = e' ↔ e ≍ e'

Tactic:
exact _root_.cast_eq_iff_heq

Premises used: cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
rw : e ≍ e' ↔ e' ≍ e
⊢ e' = cast hu hv e ↔ e' ≍ e

Tactic:
rw [eq_comm, Hom.cast_eq_iff_heq]

Premises used: eq_comm, Quiver.Hom.cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e ≍ e' ↔ e' ≍ e

Tactic:
⟨HEq.symm, HEq.symm⟩

Premises used: HEq.symm, Iff.intro
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e ≍ e' ↔ e' ≍ e

Tactic:
exact ⟨HEq.symm, HEq.symm⟩
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
rw : Path.{u, u_1} u' v = Path.{u, u_1} u' v'
rw₁ rw₂ : Path.{u, u_1} u' v' = Path.{u, u_1} u' v'
⊢ Path.{u, u_1} u v = Path.{u, u_1} u' v'

Tactic:
rw [hu, hv]
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
subst_vars : ∀ (p : Path.{u, u_1} u' v'), cast ⋯ ⋯ p = _root_.cast ⋯ p
⊢ cast hu hv p = _root_.cast ⋯ p

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u' v' : U
p : Path.{u, u_1} u' v'
⊢ cast ⋯ ⋯ p = _root_.cast ⋯ p

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v : U
p : Path.{u, u_1} u v
⊢ cast ⋯ ⋯ p = p

Tactic:
rfl

Premises used: Quiver.Path.cast, rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' u'' v'' : U
p : Path.{u, u_1} u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
subst_vars : ∀ (p : Path.{u, u_1} u'' v''), cast ⋯ ⋯ (cast ⋯ ⋯ p) = cast ⋯ ⋯ p
⊢ cast hu' hv' (cast hu hv p) = cast ⋯ ⋯ p

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u'' v'' : U
p : Path.{u, u_1} u'' v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ p) = cast ⋯ ⋯ p

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u u' : U
hu : u = u'
subst_vars : Eq (α := Path.{u, u_1} u' u') (cast ⋯ ⋯ nil) nil
⊢ Eq (α := Path.{u, u_1} u' u') (cast hu hu nil) nil

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u' : U
⊢ Eq (α := Path.{u, u_1} u' u') (cast ⋯ ⋯ nil) nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
rw : _root_.cast ⋯ p ≍ p
⊢ cast hu hv p ≍ p

Tactic:
rw [Path.cast_eq_cast]

Premises used: Quiver.Path.cast_eq_cast
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
⊢ _root_.cast ⋯ p ≍ p

Tactic:
_root_.cast_heq _ _

Premises used: cast_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
⊢ _root_.cast ⋯ p ≍ p

Tactic:
exact _root_.cast_heq _ _

Premises used: cast_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u' v'
rw : _root_.cast ⋯ p = p' ↔ p ≍ p'
⊢ cast hu hv p = p' ↔ p ≍ p'

Tactic:
rw [Path.cast_eq_cast]

Premises used: Quiver.Path.cast_eq_cast
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u' v'
⊢ _root_.cast ⋯ p = p' ↔ p ≍ p'

Tactic:
_root_.cast_eq_iff_heq

Premises used: cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u' v'
⊢ _root_.cast ⋯ p = p' ↔ p ≍ p'

Tactic:
exact _root_.cast_eq_iff_heq

Premises used: cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u' v'
⊢ p' = cast hu hv p ↔ p' ≍ p

Tactic:
⟨fun h => ((p.cast_eq_iff_heq hu hv p').1 h.symm).symm, fun h =>
    ((p.cast_eq_iff_heq hu hv p').2 h.symm).symm⟩

Premises used: Iff.mpr, HEq.symm, Iff.intro, Iff.mp, Quiver.Path.cast_eq_iff_heq, Eq.symm
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v w u' w' : U
p : Path.{u, u_1} u v
e : v ⟶ w
hu : u = u'
hw : w = w'
subst_vars : ∀ (p : Path.{u, u_1} u' v) (e : v ⟶ w'), cast ⋯ ⋯ (p.cons e) = (cast ⋯ ⋯ p).cons (Hom.cast ⋯ ⋯ e)
⊢ cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
v u' w' : U
p : Path.{u, u_1} u' v
e : v ⟶ w'
⊢ cast ⋯ ⋯ (p.cons e) = (cast ⋯ ⋯ p).cons (Hom.cast ⋯ ⋯ e)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
rw : p ≍ p'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
rw [Path.cast_eq_iff_heq]

Premises used: Quiver.Path.cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
heq_of_cons_eq_cons h

Premises used: Quiver.Path.heq_of_cons_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ p ≍ p'

Tactic:
exact heq_of_cons_eq_cons h

Premises used: Quiver.Path.heq_of_cons_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
rw : e ≍ e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
rw [Hom.cast_eq_iff_heq]

Premises used: Quiver.Hom.cast_eq_iff_heq
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
hom_heq_of_cons_eq_cons h

Premises used: Quiver.Path.hom_heq_of_cons_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v v' w : U
p : Path.{u, u_1} u v
p' : Path.{u, u_1} u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ e ≍ e'

Tactic:
exact hom_heq_of_cons_eq_cons h

Premises used: Quiver.Path.hom_heq_of_cons_eq_cons
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v : U
p : Path.{u, u_1} u v
hzero : p.length = 0
nil :
  ∀ (hzero : length.{u_1, u} (V := U) (a := u) Path.nil = 0),
    Eq (α := Path.{u, u_1} u u) (Path.cast ⋯ ⋯ Path.nil) Path.nil
cons :
  ∀ {b : U} (a : Path.{u, u_1} u b) (a_1 : b ⟶ v) (hzero : (a.cons a_1).length = 0),
    Path.cast ⋯ ⋯ (a.cons a_1) = Path.nil
⊢ Path.cast ⋯ ⋯ p = Path.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u : U
hzero : length.{u_1, u} (V := U) (a := u) nil = 0
⊢ Eq (α := Path.{u, u_1} u u) (Path.cast ⋯ ⋯ nil) nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Cast
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v b : U
a : Path.{u, u_1} u b
a_1 : b ⟶ v
hzero : (a.cons a_1).length = 0
⊢ Path.cast ⋯ ⋯ (a.cons a_1) = nil

Tactic:
simp only [Nat.succ_ne_zero, length_cons] at hzero

Premises used: Quiver.Path.length_cons, Nat.succ_ne_zero
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_1
inst : Quiver.{u, u_1} V
a b : V
⊢ Eq (α := WeaklyConnectedComponent.{u, u_1} V) (WeaklyConnectedComponent.mk a) (WeaklyConnectedComponent.mk b) ↔
    Nonempty (Path.{u, u_1} a b)

Tactic:
Quotient.eq''

Premises used: Quotient.eq'', Quotient.mk', Quiver.WeaklyConnectedComponent, Quiver.WeaklyConnectedComponent.mk
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
⊢ IsStronglyConnected.{u_2, u_3} V ↔ ∀ (i j : V), Nonempty (Path.{u_3, u_2} i j)

Tactic:
Iff.rfl

Premises used: Quiver.IsStronglyConnected, Iff.rfl
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
⊢ IsSStronglyConnected.{u_2, u_3} V ↔ ∀ (i j : V), ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
Iff.rfl

Premises used: Iff.rfl, Quiver.IsSStronglyConnected
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
i j : V
⊢ Nonempty (Path.{u_3, u_2} i j)

Tactic:
h i j
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i j : V
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
h i j
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i : V
⊢ ∃ (p : Path.{u_3, u_2} i i), 0 < p.length

Tactic:
h i i
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i j : V
obtain : ∀ (p : Path.{u_3, u_2} i j), 0 < p.length → Nonempty (Path.{u_3, u_2} i j)
⊢ Nonempty (Path.{u_3, u_2} i j)

Tactic:
obtain ⟨p, _⟩ := h i j
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i j : V
p : Path.{u_3, u_2} i j
h_1 : 0 < p.length
⊢ Nonempty (Path.{u_3, u_2} i j)

Tactic:
⟨p⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i j : V
p : Path.{u_3, u_2} i j
h_1 : 0 < p.length
⊢ Nonempty (Path.{u_3, u_2} i j)

Tactic:
exact ⟨p⟩
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
⊢ Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk a)
      (StronglyConnectedComponent.mk b) ↔
    Nonempty (Path.{u_3, u_2} a b) ∧ Nonempty (Path.{u_3, u_2} b a)

Tactic:
Quotient.eq''

Premises used: Quiver.StronglyConnectedComponent, Quotient.eq'', Quotient.mk', Quiver.StronglyConnectedComponent.mk
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
⊢ Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk a)
      (StronglyConnectedComponent.mk b) ↔
    Nonempty (Path.{u_3, u_2} a b) ∧ Nonempty (Path.{u_3, u_2} b a)

Tactic:
StronglyConnectedComponent.eq a b

Premises used: Quiver.StronglyConnectedComponent.eq
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
v : V
⊢ ∃ (p : Path.{u_3, u_2} v v), 0 < p.length

Tactic:
h v v
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
hab : Nonempty (Path.{u_3, u_2} a b)
hba : Nonempty (Path.{u_3, u_2} b a)
⊢ Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk a) (StronglyConnectedComponent.mk b)

Tactic:
(StronglyConnectedComponent.eq (a := a) (b := b)).2 ⟨hab, hba⟩

Premises used: Iff.mpr, Quiver.StronglyConnectedComponent.eq, And.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
a b : V
h :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk a) (StronglyConnectedComponent.mk b)
⊢ Nonempty (Path.{u_3, u_2} a b) ∧ Nonempty (Path.{u_3, u_2} b a)

Tactic:
(StronglyConnectedComponent.eq (a := a) (b := b)).1 h

Premises used: Quiver.StronglyConnectedComponent.eq, Iff.mp
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
mp :
  (∀ (w : V),
      Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
          (StronglyConnectedComponent.mk v) →
        w = v) →
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
mpr :
  (∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))) →
    ∀ (w : V),
      Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
          (StronglyConnectedComponent.mk v) →
        w = v
⊢ (∀ (w : V),
      Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
          (StronglyConnectedComponent.mk v) →
        w = v) ↔
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
h_bidir : Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v)
⊢ Nonempty (Path.{u_3, u_2} v w)

Tactic:
obtain ⟨hab, hba⟩ := h_bidir
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
h_bidir : Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v)
hab : Nonempty (Path.{u_3, u_2} v w)
⊢ Nonempty (Path.{u_3, u_2} w v)

Tactic:
obtain ⟨hab, hba⟩ := h_bidir
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path.{u_3, u_2} v w)
hba : Nonempty (Path.{u_3, u_2} w v)
⊢ Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)

Tactic:
have h_same_scc : (w : StronglyConnectedComponent V) = v :=
      stronglyConnectedComponent_eq_of_path (a := w) (b := v) hba hab
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path.{u_3, u_2} v w)
hba : Nonempty (Path.{u_3, u_2} w v)
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
⊢ v ≠ v

Tactic:
obtain ⟨rfl⟩ := h_singleton w h_same_scc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path.{u_3, u_2} v w)
hba : Nonempty (Path.{u_3, u_2} w v)
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne₁ : v ≠ v
⊢ Nonempty (Path.{u_3, u_2} v v)

Tactic:
obtain ⟨rfl⟩ := h_singleton w h_same_scc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path.{u_3, u_2} v w)
hba : Nonempty (Path.{u_3, u_2} w v)
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne₁ : v ≠ v
hab₁ : Nonempty (Path.{u_3, u_2} v v)
⊢ Nonempty (Path.{u_3, u_2} v v)

Tactic:
obtain ⟨rfl⟩ := h_singleton w h_same_scc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
w : V
hw_ne : w ≠ v
hab : Nonempty (Path.{u_3, u_2} v w)
hba : Nonempty (Path.{u_3, u_2} w v)
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne₁ : v ≠ v
hab₁ hba₁ : Nonempty (Path.{u_3, u_2} v v)
⊢ Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk v) (StronglyConnectedComponent.mk v)

Tactic:
obtain ⟨rfl⟩ := h_singleton w h_same_scc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_singleton :
  ∀ (w : V),
    Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w)
        (StronglyConnectedComponent.mk v) →
      w = v
hw_ne : v ≠ v
hab hba : Nonempty (Path.{u_3, u_2} v v)
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk v) (StronglyConnectedComponent.mk v)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
w : V
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
mpr : ∀ (hw_ne : ¬w = v), False
⊢ w = v

Tactic:
by_contra hw_ne
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
w : V
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne : ¬w = v
⊢ Nonempty (Path.{u_3, u_2} w v)

Tactic:
obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc

Premises used: Quiver.exists_path_of_stronglyConnectedComponent_eq
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
w : V
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne : ¬w = v
hab : Nonempty (Path.{u_3, u_2} w v)
⊢ Nonempty (Path.{u_3, u_2} v w)

Tactic:
obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc

Premises used: Quiver.exists_path_of_stronglyConnectedComponent_eq
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
w : V
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne : ¬w = v
hab : Nonempty (Path.{u_3, u_2} w v)
hba : Nonempty (Path.{u_3, u_2} v w)
⊢ False

Tactic:
(h_no_bidir w hw_ne) ⟨hba, hab⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path.{u_3, u_2} v w) ∧ Nonempty (Path.{u_3, u_2} w v))
w : V
h_same_scc :
  Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk w) (StronglyConnectedComponent.mk v)
hw_ne : ¬w = v
hab : Nonempty (Path.{u_3, u_2} w v)
hba : Nonempty (Path.{u_3, u_2} v w)
⊢ False

Tactic:
exact (h_no_bidir w hw_ne) ⟨hba, hab⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b : Symmetrify V
obtain : ∀ (p : Path.{u_3, u_2} a b), Nonempty (Path.{u_3, u_2} a b)
⊢ Nonempty (Path.{u_3, u_2} a b)

Tactic:
obtain ⟨p⟩ := h a b
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b : Symmetrify V
⊢ Nonempty (Path.{u_3, u_2} a a)

Tactic:
⟨Path.nil⟩

Premises used: Quiver.Path.nil, Nonempty.intro
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b : Symmetrify V
⊢ Nonempty (Path.{u_3, u_2} a a)

Tactic:
exact ⟨Path.nil⟩
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b b_1 c : Symmetrify V
q : Path.{u_3, u_2} a b_1
e : b_1 ⟶ c
ih : Nonempty (Path.{u_3, u_2} a b_1)
⊢ Nonempty (Path.{u_3, u_2} a c)

Tactic:
⟨ih.some.cons (Sum.inl e)⟩

Premises used: Nonempty.some, Sum.inl, Nonempty.intro, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b b_1 c : Symmetrify V
q : Path.{u_3, u_2} a b_1
e : b_1 ⟶ c
ih : Nonempty (Path.{u_3, u_2} a b_1)
⊢ Nonempty (Path.{u_3, u_2} a c)

Tactic:
exact ⟨ih.some.cons (Sum.inl e)⟩
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsStronglyConnected.{u_2, u_3} V
a b : Symmetrify V
p : Path.{u_3, u_2} a b
nil : Nonempty (Path.{u_3, u_2} a a)
cons :
  ∀ {b c : Symmetrify V} (q : Path.{u_3, u_2} a b) (e : b ⟶ c) (ih : Nonempty (Path.{u_3, u_2} a b)),
    Nonempty (Path.{u_3, u_2} a c)
⊢ Nonempty (Path.{u_3, u_2} a b)

Tactic:
induction p with
  | nil => exact ⟨Path.nil⟩
  | cons q e ih => exact ⟨ih.some.cons (Sum.inl e)⟩
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
obtain : ∀ (p₁ : Path.{u_3, u_2} i i₀), ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
obtain ⟨p₁⟩ := h_sc i i₀
-- Module: Mathlib.Combinatorics.Quiver.ConnectedComponent
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h_sc : IsStronglyConnected.{u_2, u_3} V
i₀ j₀ : V
e₀ : i₀ ⟶ j₀
i j : V
p₁ : Path.{u_3, u_2} i i₀
obtain : ∀ (p₂ : Path.{u_3, u_2} j₀ j), ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length

Tactic:
obtain ⟨p₂⟩ := h_sc j₀ j