awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h j : shortestPath r c = p.cons e
⊢ a = a ∧
    HEq (α := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯) (β := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
have refl : a = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
a c : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
e : a ⟶ c
p : Path.{v, u} r a
h j : shortestPath r c = p.cons e
refl : a = a
⊢ a = a ∧
    HEq (α := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯) (β := a ⟶ c)
      (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e ⋯)
have refl₁ : HEq (α := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e sorry)
  (β := a ⟶ c) (Subtype.mk (p := fun (f : a ⟶ c) ↦ Membership.mem (γ := Set (a ⟶ c)) (geodesicSubtree r a c) f) e sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
⊢ b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)
have nil : ∀ (hp : Eq (α := Path.{v, u} r r) (shortestPath r r) Path.nil),
  r = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ r)
Tactic: rcases hp : shortestPath r b with (_ | ⟨p, e⟩)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Arborescence (goal)
Goal:
V : Type u
inst : Quiver.{v, u} V
r : V
inst_1 : RootedConnected.{u, v} r
b : WideSubquiver.toType.{u, v} V (geodesicSubtree r)
nil :
  ∀ (hp : Eq (α := Path.{v, u} r r) (shortestPath r r) Path.nil),
    r = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ r)
⊢ b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)
have cons : ∀ {b_1 : V} (p : Path.{v, u} r b_1) (e : b_1 ⟶ b) (hp : shortestPath r b = p.cons e),
  b = r ∨ ∃ (a : WideSubquiver.toType.{u, v} V (geodesicSubtree r)), Nonempty.{v + 1} (a ⟶ b)
Tactic: rcases hp : shortestPath r b with (_ | ⟨p, e⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ (u ⟶ v) = (u' ⟶ v')
have rw : (u' ⟶ v) = (u' ⟶ v')
Tactic: rw [hu, hv]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
rw : (u' ⟶ v) = (u' ⟶ v')
⊢ (u ⟶ v) = (u' ⟶ v')
have rw₁ : (u' ⟶ v') = (u' ⟶ v')
Tactic: rw [hu, hv]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ (u ⟶ v) = (u' ⟶ v')
have this : (u' ⟶ v) = (u' ⟶ v')
Tactic: {rw [hu, hv]}
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
this : (u' ⟶ v) = (u' ⟶ v')
⊢ (u ⟶ v) = (u' ⟶ v')
have this₁ : (u' ⟶ v') = (u' ⟶ v')
Tactic: {rw [hu, hv]}
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ cast hu hv e = _root_.cast ⋯ e
have subst_vars : ∀ (e : u' ⟶ v'), cast sorry sorry e = _root_.cast sorry e
Tactic: subst_vars
Cleared hypotheses: u, v, hu, hv, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast ⋯ ⋯ e
have subst_vars : ∀ (e : u'' ⟶ v''), cast sorry sorry (cast sorry sorry e) = cast sorry sorry e
Tactic: subst_vars
Cleared hypotheses: u, v, u', v', e, hu, hv, hu', hv'
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ cast hu hv e ≍ e
have subst_vars : ∀ (e : u' ⟶ v'), cast sorry sorry e ≍ e
Tactic: subst_vars
Cleared hypotheses: u, v, hu, hv, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ cast hu hv e = e' ↔ e ≍ e'
have rw : _root_.cast sorry e = e' ↔ e ≍ e'
Tactic: rw [Hom.cast_eq_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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' = cast hu hv e ↔ e' ≍ e
have rw : e ≍ e' ↔ e' ≍ e
Tactic: rw [eq_comm, Hom.cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ Path.{u, u_1} u v = Path.{u, u_1} u' v'
have rw : Path.{u, u_1} u' v = Path.{u, u_1} u' v'
Tactic: rw [hu, hv]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ Path.{u, u_1} u v = Path.{u, u_1} u' v'
have rw₁ : Path.{u, u_1} u' v' = Path.{u, u_1} u' v'
Tactic: rw [hu, hv]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ cast hu hv p = _root_.cast ⋯ p
have subst_vars : ∀ (p : Path.{u, u_1} u' v'), cast sorry sorry p = _root_.cast sorry p
Tactic: subst_vars
Cleared hypotheses: u, v, hu, hv, p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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''
⊢ cast hu' hv' (cast hu hv p) = cast ⋯ ⋯ p
have subst_vars : ∀ (p : Path.{u, u_1} u'' v''), cast sorry sorry (cast sorry sorry p) = cast sorry sorry p
Tactic: subst_vars
Cleared hypotheses: u, v, u', v', p, hu, hv, hu', hv'
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
u u' : U
hu : u = u'
⊢ Eq (α := Path.{u, u_1} u' u') (cast hu hu nil) nil
have subst_vars : Eq (α := Path.{u, u_1} u' u') (cast sorry sorry nil) nil
Tactic: subst_vars
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ cast hu hv p ≍ p
have rw : _root_.cast sorry p ≍ p
Tactic: rw [Path.cast_eq_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ cast hu hv p = p' ↔ p ≍ p'
have rw : _root_.cast sorry p = p' ↔ p ≍ p'
Tactic: rw [Path.cast_eq_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)
have subst_vars : ∀ (p : Path.{u, u_1} u' v) (e : v ⟶ w'), cast sorry sorry (p.cons e) = (cast sorry sorry p).cons (Hom.cast sorry sorry e)
Tactic: subst_vars
Cleared hypotheses: u, w, p, e, hu, hw
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ Path.cast ⋯ ⋯ p = p'
have rw : p ≍ p'
Tactic: rw [Path.cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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'
⊢ Hom.cast ⋯ ⋯ e = e'
have rw : e ≍ e'
Tactic: rw [Hom.cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ Path.cast ⋯ ⋯ p = nil
have nil : ∀ (hzero : length.{u_1, u} (V := U) (a := u) nil = 0), Eq (α := Path.{u, u_1} u u) (Path.cast sorry sorry nil) nil
Tactic: cases p
Cleared hypotheses: v, p, hzero
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Cast (goal)
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
⊢ Path.cast ⋯ ⋯ p = Path.nil
have cons : ∀ {b : U} (a : Path.{u, u_1} u b) (a_1 : b ⟶ v) (hzero : (a.cons a_1).length = 0), Path.cast sorry sorry (a.cons a_1) = Path.nil
Tactic: cases p
Cleared hypotheses: p, hzero
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
h : IsSStronglyConnected.{u_2, u_3} V
i j : V
⊢ Nonempty (Path.{u_3, u_2} i j)
have obtain : ∀ (p : Path.{u_3, u_2} i j), 0 < p.length → Nonempty (Path.{u_3, u_2} i j)
Tactic: obtain ⟨p, _⟩ := h i j
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
Goal:
V : Type u_2
inst : Quiver.{u_3, u_2} V
v : 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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))
⊢ (∀ (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))
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have hab : Nonempty (Path.{u_3, u_2} v w)
Tactic: obtain ⟨hab, hba⟩ := h_bidir
Cleared hypotheses: h_bidir
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have hba : Nonempty (Path.{u_3, u_2} w v)
Tactic: obtain ⟨hab, hba⟩ := h_bidir
Cleared hypotheses: h_bidir
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have h_same_scc : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have hw_ne₁ : v ≠ v
Tactic: obtain ⟨rfl⟩ := h_singleton w h_same_scc
Cleared hypotheses: w, hw_ne, hab, hba, h_same_scc
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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
⊢ False
have hab₁ : Nonempty (Path.{u_3, u_2} v v)
Tactic: obtain ⟨rfl⟩ := h_singleton w h_same_scc
Cleared hypotheses: w, hw_ne, hab, hba, h_same_scc
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have h_same_scc₁ : Eq (α := StronglyConnectedComponent.{u_2, u_3} V) (StronglyConnectedComponent.mk v) (StronglyConnectedComponent.mk v)
Tactic: obtain ⟨rfl⟩ := h_singleton w h_same_scc
Cleared hypotheses: w, hw_ne, hab, hba, h_same_scc
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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)
⊢ w = v
have mpr : ∀ (hw_ne : ¬w = v), False
Tactic: by_contra hw_ne
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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
⊢ False
have hab : Nonempty (Path.{u_3, u_2} w v)
Tactic: obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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)
⊢ False
have hba : Nonempty (Path.{u_3, u_2} v w)
Tactic: obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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 b)
have obtain : ∀ (p : Path.{u_3, u_2} a b), Nonempty (Path.{u_3, u_2} a b)
Tactic: obtain ⟨p⟩ := h a b
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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
⊢ Nonempty (Path.{u_3, u_2} a b)
have nil : Nonempty (Path.{u_3, u_2} a a)
Tactic: induction p with
  | nil => exact ⟨Path.nil⟩
  | cons q e ih => exact ⟨ih.some.cons (Sum.inl e)⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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)
⊢ Nonempty (Path.{u_3, u_2} a b)
have 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)
Tactic: induction p with
  | nil => exact ⟨Path.nil⟩
  | cons q e ih => exact ⟨ih.some.cons (Sum.inl e)⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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 j), 0 < p.length
have obtain : ∀ (p₁ : Path.{u_3, u_2} i i₀), ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
Tactic: obtain ⟨p₁⟩ := h_sc i i₀
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (goal)
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₀
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
have obtain : ∀ (p₂ : Path.{u_3, u_2} j₀ j), ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
Tactic: obtain ⟨p₂⟩ := h_sc j₀ j
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.ConnectedComponent (hypothesis)
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₀
p₂ : Path.{u_3, u_2} j₀ j
p : Path.{u_3, u_2} i j := p₁.comp (e₀.toPath.comp p₂)
⊢ ∃ (p : Path.{u_3, u_2} i j), 0 < p.length
have hp_pos : 0 < p.length
Tactic: have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (hypothesis)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : Eq.{v + 1} (α := φ.obj u ⟶ φ.obj v) ((fun (f : u ⟶ v) ↦ φ.map f) f) ((fun (f : u ⟶ v) ↦ φ.map f) g)
⊢ f = g
have this : φ.star u (Star.mk f) = φ.star u (Star.mk g)
Tactic: have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
⊢ ψ.IsCovering
have refine_1 : ∀ (v : V), Bijective (ψ.star v)
Tactic: refine ⟨fun v => ?_, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
refine_1 : ∀ (v : V), Bijective (ψ.star v)
⊢ ψ.IsCovering
have refine_2 : ∀ (v : V), Bijective (ψ.costar v)
Tactic: refine ⟨fun v => ?_, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.star v)
have refine_1 : ∀ (u : U), Bijective (α := Star.{v, u_2} (φ.obj u)) (ψ.star (φ.obj u))
Tactic: obtain ⟨u, rfl⟩ := φsur v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
W : Type u_3
inst_2 : Quiver.{w, u_3} W
ψ : Prefunctor.{v, w, u_2, u_3} V W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
v : V
⊢ Bijective (ψ.costar v)
have refine_2 : ∀ (u : U), Bijective (α := Costar.{v, u_2} (φ.obj u)) (ψ.costar (φ.obj u))
Tactic: obtain ⟨u, rfl⟩ := φsur v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
⊢ φ.symmetrify.star u =
    (⇑(Equiv.symm (Quiver.symmetrifyStar (φ.obj u))) :
        (a : Star (φ.obj u) ⊕ Costar (φ.obj u)) → Star (Symmetrify.of.obj (φ.obj u))) ∘
      Sum.map (φ.star u) (φ.costar u) ∘
        (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
have rw : (⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
    φ.symmetrify.star u =
  Sum.map (φ.star u) (φ.costar u) ∘ (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
Tactic: rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyStar (φ.obj u))]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Covering (goal)
Goal:
U : Type u_1
inst : Quiver.{u, u_1} U
V : Type u_2
inst_1 : Quiver.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
u : U
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
      φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
have h : ∀ (v : Symmetrify U) (f : u ⟶ v),
  ((⇑(Quiver.symmetrifyStar (φ.obj u)) : (a : Star (Symmetrify.of.obj (φ.obj u))) → Star (φ.obj u) ⊕ Costar (φ.obj u)) ∘
        φ.symmetrify.star u)
      (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f)) =
    Function.comp (α := Star.{u, u_1} (obj.{u, u, u_1, u_1} Symmetrify.of u)) (Sum.map (φ.star u) (φ.costar u))
      (⇑(Quiver.symmetrifyStar u) : (a : Star (Symmetrify.of.obj u)) → Star u ⊕ Costar u)
      (Sigma.mk (β := fun (v : Symmetrify U) ↦ u ⟶ v) v (Sum.inl f))
Tactic: ext ⟨v, f | g⟩