[GOAL]
s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')
[PROOFSTEP]
simp [xgcdAux]
[GOAL]
r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
[GOAL]
case intro
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < succ r
⊢ xgcdAux (succ r) s t r' s' t' =
    xgcdAux (r' % succ r) (s' - ↑r' / ↑(succ r) * s) (t' - ↑r' / ↑(succ r) * t) (succ r) s t
[PROOFSTEP]
rfl
[GOAL]
s : ℕ
⊢ gcdA 0 s = 0
[PROOFSTEP]
unfold gcdA
[GOAL]
s : ℕ
⊢ (xgcd 0 s).fst = 0
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]
[GOAL]
s : ℕ
⊢ gcdB 0 s = 1
[PROOFSTEP]
unfold gcdB
[GOAL]
s : ℕ
⊢ (xgcd 0 s).snd = 1
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]
[GOAL]
s : ℕ
h : s ≠ 0
⊢ gcdA s 0 = 1
[PROOFSTEP]
unfold gcdA xgcd
[GOAL]
s : ℕ
h : s ≠ 0
⊢ (xgcdAux s 1 0 0 0 1).snd.fst = 1
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
[GOAL]
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (succ s) 1 0 0 0 1).snd.fst = 1
[PROOFSTEP]
rw [xgcdAux_succ]
[GOAL]
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.fst = 1
[PROOFSTEP]
rfl
[GOAL]
s : ℕ
h : s ≠ 0
⊢ gcdB s 0 = 0
[PROOFSTEP]
unfold gcdB xgcd
[GOAL]
s : ℕ
h : s ≠ 0
⊢ (xgcdAux s 1 0 0 0 1).snd.snd = 0
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
[GOAL]
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (succ s) 1 0 0 0 1).snd.snd = 0
[PROOFSTEP]
rw [xgcdAux_succ]
[GOAL]
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.snd = 0
[PROOFSTEP]
rfl
[GOAL]
x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').fst = gcd 0 n
[PROOFSTEP]
simp
[GOAL]
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : ℤ
⊢ (xgcdAux x s t y s' t').fst = gcd x y
[PROOFSTEP]
simp [xgcdAux_rec, h, IH]
[GOAL]
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : ℤ
⊢ gcd (y % x) x = gcd x y
[PROOFSTEP]
rw [← gcd_rec]
[GOAL]
x y : ℕ
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
[PROOFSTEP]
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
[GOAL]
x y : ℕ
⊢ xgcd x y = (gcdA x y, gcdB x y)
[PROOFSTEP]
unfold gcdA gcdB
[GOAL]
x y : ℕ
⊢ xgcd x y = ((xgcd x y).fst, (xgcd x y).snd)
[PROOFSTEP]
cases xgcd x y
[GOAL]
case mk
x y : ℕ
fst✝ snd✝ : ℤ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
[PROOFSTEP]
rfl
[GOAL]
x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (r, s, t) → Nat.P x y (r', s', t') → Nat.P x y (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using gcd.induction with
| H0 => simp
| H1 a b h IH =>
  intro s t s' t' p p'
  rw [xgcdAux_rec h]; refine' IH _ p; dsimp [P] at *
  rw [Int.emod_def]; generalize (b / a : ℤ) = k
  rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s, ← mul_assoc, ← mul_assoc,
    add_comm (x * s * k), ← add_sub_assoc, sub_sub]
[GOAL]
x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (r, s, t) → Nat.P x y (r', s', t') → Nat.P x y (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using gcd.induction with
| H0 => simp
| H1 a b h IH =>
  intro s t s' t' p p'
  rw [xgcdAux_rec h]; refine' IH _ p; dsimp [P] at *
  rw [Int.emod_def]; generalize (b / a : ℤ) = k
  rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s, ← mul_assoc, ← mul_assoc,
    add_comm (x * s * k), ← add_sub_assoc, sub_sub]
[GOAL]
case H0
x y n✝ : ℕ
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (0, s, t) → Nat.P x y (n✝, s', t') → Nat.P x y (xgcdAux 0 s t n✝ s' t')
[PROOFSTEP]

| H0 => simp
[GOAL]
case H0
x y n✝ : ℕ
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (0, s, t) → Nat.P x y (n✝, s', t') → Nat.P x y (xgcdAux 0 s t n✝ s' t')
[PROOFSTEP]
simp
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, Nat.P x y (b % a, s, t) → Nat.P x y (a, s', t') → Nat.P x y (xgcdAux (b % a) s t a s' t')
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (a, s, t) → Nat.P x y (b, s', t') → Nat.P x y (xgcdAux a s t b s' t')
[PROOFSTEP]

| H1 a b h IH =>
  intro s t s' t' p p'
  rw [xgcdAux_rec h]; refine' IH _ p; dsimp [P] at *
  rw [Int.emod_def]; generalize (b / a : ℤ) = k
  rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s, ← mul_assoc, ← mul_assoc,
    add_comm (x * s * k), ← add_sub_assoc, sub_sub]
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, Nat.P x y (b % a, s, t) → Nat.P x y (a, s', t') → Nat.P x y (xgcdAux (b % a) s t a s' t')
⊢ ∀ {s t s' t' : ℤ}, Nat.P x y (a, s, t) → Nat.P x y (b, s', t') → Nat.P x y (xgcdAux a s t b s' t')
[PROOFSTEP]
intro s t s' t' p p'
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, Nat.P x y (b % a, s, t) → Nat.P x y (a, s', t') → Nat.P x y (xgcdAux (b % a) s t a s' t')
s t s' t' : ℤ
p : Nat.P x y (a, s, t)
p' : Nat.P x y (b, s', t')
⊢ Nat.P x y (xgcdAux a s t b s' t')
[PROOFSTEP]
rw [xgcdAux_rec h]
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, Nat.P x y (b % a, s, t) → Nat.P x y (a, s', t') → Nat.P x y (xgcdAux (b % a) s t a s' t')
s t s' t' : ℤ
p : Nat.P x y (a, s, t)
p' : Nat.P x y (b, s', t')
⊢ Nat.P x y (xgcdAux (b % a) (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
[PROOFSTEP]
refine' IH _ p
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, Nat.P x y (b % a, s, t) → Nat.P x y (a, s', t') → Nat.P x y (xgcdAux (b % a) s t a s' t')
s t s' t' : ℤ
p : Nat.P x y (a, s, t)
p' : Nat.P x y (b, s', t')
⊢ Nat.P x y (b % a, s' - ↑b / ↑a * s, t' - ↑b / ↑a * t)
[PROOFSTEP]
dsimp [P] at *
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑(xgcdAux (b % a) s t a s' t').fst =
          ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b % ↑a = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
[PROOFSTEP]
rw [Int.emod_def]
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑(xgcdAux (b % a) s t a s' t').fst =
          ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
[PROOFSTEP]
generalize (b / a : ℤ) = k
[GOAL]
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑(xgcdAux (b % a) s t a s' t').fst =
          ↑x * (xgcdAux (b % a) s t a s' t').2.fst + ↑y * (xgcdAux (b % a) s t a s' t').2.snd
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)
[PROOFSTEP]
rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s, ← mul_assoc, ← mul_assoc,
  add_comm (x * s * k), ← add_sub_assoc, sub_sub]
[GOAL]
x y : ℕ
⊢ ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
[PROOFSTEP]
have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
[GOAL]
x y : ℕ
⊢ Nat.P x y (x, 1, 0)
[PROOFSTEP]
simp [P]
[GOAL]
x y : ℕ
⊢ Nat.P x y (y, 0, 1)
[PROOFSTEP]
simp [P]
[GOAL]
x y : ℕ
this : Nat.P x y (xgcdAux x 1 0 y 0 1)
⊢ ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
[PROOFSTEP]
rwa [xgcdAux_val, xgcd_val] at this
[GOAL]
k n : ℕ
hk : gcd n k < k
⊢ ∃ m, n * m % k = gcd n k
[PROOFSTEP]
have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))
[GOAL]
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
⊢ ∃ m, n * m % k = gcd n k
[PROOFSTEP]
have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)
[GOAL]
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : (fun m => Int.toNat (m % ↑k)) ↑(gcd n k) = (fun m => Int.toNat (m % ↑k)) (↑n * gcdA n k + ↑k * gcdB n k)
⊢ ∃ m, n * m % k = gcd n k
[PROOFSTEP]
simp only at key
[GOAL]
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)
⊢ ∃ m, n * m % k = gcd n k
[PROOFSTEP]
rw [Int.add_mul_emod_self_left, ← Int.coe_nat_mod, Int.toNat_coe_nat, mod_eq_of_lt hk] at key
[GOAL]
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ ∃ m, n * m % k = gcd n k
[PROOFSTEP]
refine' ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj _) key.symm⟩
[GOAL]
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
[PROOFSTEP]
rw [Int.ofNat_eq_coe, Int.coe_nat_mod, Int.ofNat_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.ofNat_eq_coe,
  Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
[GOAL]
m n : ℕ
⊢ ↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + -(↑n + 1) * -Nat.gcdB (natAbs ↑m) (Nat.succ n)
[PROOFSTEP]
rw [neg_mul_neg]
[GOAL]
m n : ℕ
⊢ ↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
[PROOFSTEP]
apply Nat.gcd_eq_gcd_ab
[GOAL]
m n : ℕ
⊢ ↑(gcd -[m+1] ↑n) = -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
[PROOFSTEP]
rw [neg_mul_neg]
[GOAL]
m n : ℕ
⊢ ↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
[PROOFSTEP]
apply Nat.gcd_eq_gcd_ab
[GOAL]
m n : ℕ
⊢ ↑(gcd -[m+1] -[n+1]) =
    -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
[PROOFSTEP]
rw [neg_mul_neg, neg_mul_neg]
[GOAL]
m n : ℕ
⊢ ↑(gcd -[m+1] -[n+1]) =
    (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + (↑n + 1) * Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
[PROOFSTEP]
apply Nat.gcd_eq_gcd_ab
[GOAL]
a b : ℤ
H : b ∣ a
⊢ natAbs (a / b) = natAbs a / natAbs b
[PROOFSTEP]
rcases Nat.eq_zero_or_pos (natAbs b) with (h | h)
[GOAL]
case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / b) = natAbs a / natAbs b
[PROOFSTEP]
rw [natAbs_eq_zero.1 h]
[GOAL]
case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / 0) = natAbs a / natAbs 0
[PROOFSTEP]
simp [Int.ediv_zero]
[GOAL]
case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
[PROOFSTEP]
calc
  natAbs (a / b) = natAbs (a / b) * 1 := by rw [mul_one]
  _ = natAbs (a / b) * (natAbs b / natAbs b) := by rw [Nat.div_self h]
  _ = natAbs (a / b) * natAbs b / natAbs b := by rw [Nat.mul_div_assoc _ dvd_rfl]
  _ = natAbs (a / b * b) / natAbs b := by rw [natAbs_mul (a / b) b]
  _ = natAbs a / natAbs b := by rw [Int.ediv_mul_cancel H]
[GOAL]
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs (a / b) * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * 1 = natAbs (a / b) * (natAbs b / natAbs b)
[PROOFSTEP]
rw [Nat.div_self h]
[GOAL]
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * (natAbs b / natAbs b) = natAbs (a / b) * natAbs b / natAbs b
[PROOFSTEP]
rw [Nat.mul_div_assoc _ dvd_rfl]
[GOAL]
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * natAbs b / natAbs b = natAbs (a / b * b) / natAbs b
[PROOFSTEP]
rw [natAbs_mul (a / b) b]
[GOAL]
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b * b) / natAbs b = natAbs a / natAbs b
[PROOFSTEP]
rw [Int.ediv_mul_cancel H]
[GOAL]
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
l : ℤ
H1 : k * j = k * i * l
⊢ i ∣ j
[PROOFSTEP]
rw [mul_assoc] at H1
[GOAL]
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
l : ℤ
H1 : k * j = k * (i * l)
⊢ i ∣ j
[PROOFSTEP]
exact ⟨_, mul_left_cancel₀ k_non_zero H1⟩
[GOAL]
i j k : ℤ
k_non_zero : k ≠ 0
H : i * k ∣ j * k
⊢ i ∣ j
[PROOFSTEP]
rw [mul_comm i k, mul_comm j k] at H
[GOAL]
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
⊢ i ∣ j
[PROOFSTEP]
exact dvd_of_mul_dvd_mul_left k_non_zero H
[GOAL]
i j : ℤ
⊢ gcd i j * lcm i j = natAbs (i * j)
[PROOFSTEP]
rw [Int.gcd, Int.lcm, Nat.gcd_mul_lcm, natAbs_mul]
[GOAL]
i : ℤ
⊢ gcd i i = natAbs i
[PROOFSTEP]
simp [gcd]
[GOAL]
i : ℤ
⊢ gcd 0 i = natAbs i
[PROOFSTEP]
simp [gcd]
[GOAL]
i : ℤ
⊢ gcd i 0 = natAbs i
[PROOFSTEP]
simp [gcd]
[GOAL]
x y : ℤ
⊢ gcd x (-y) = gcd x y
[PROOFSTEP]
rw [Int.gcd, Int.gcd, natAbs_neg]
[GOAL]
x y : ℤ
⊢ gcd (-x) y = gcd x y
[PROOFSTEP]
rw [Int.gcd, Int.gcd, natAbs_neg]
[GOAL]
i j k : ℤ
⊢ gcd (i * j) (i * k) = natAbs i * gcd j k
[PROOFSTEP]
rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
[GOAL]
i j k : ℤ
⊢ Nat.gcd (natAbs i * natAbs j) (natAbs i * natAbs k) = natAbs i * Nat.gcd (natAbs j) (natAbs k)
[PROOFSTEP]
apply Nat.gcd_mul_left
[GOAL]
i j k : ℤ
⊢ gcd (i * j) (k * j) = gcd i k * natAbs j
[PROOFSTEP]
rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
[GOAL]
i j k : ℤ
⊢ Nat.gcd (natAbs i * natAbs j) (natAbs k * natAbs j) = Nat.gcd (natAbs i) (natAbs k) * natAbs j
[PROOFSTEP]
apply Nat.gcd_mul_right
[GOAL]
i j : ℤ
⊢ gcd i j = 0 ↔ i = 0 ∧ j = 0
[PROOFSTEP]
rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero]
[GOAL]
i j k : ℤ
H1 : k ∣ i
H2 : k ∣ j
⊢ gcd (i / k) (j / k) = gcd i j / natAbs k
[PROOFSTEP]
rw [gcd, natAbs_ediv i k H1, natAbs_ediv j k H2]
[GOAL]
i j k : ℤ
H1 : k ∣ i
H2 : k ∣ j
⊢ Nat.gcd (natAbs i / natAbs k) (natAbs j / natAbs k) = gcd i j / natAbs k
[PROOFSTEP]
exact Nat.gcd_div (natAbs_dvd_natAbs.mpr H1) (natAbs_dvd_natAbs.mpr H2)
[GOAL]
i j : ℤ
H : 0 < gcd i j
⊢ gcd (i / ↑(gcd i j)) (j / ↑(gcd i j)) = 1
[PROOFSTEP]
rw [gcd_div (gcd_dvd_left i j) (gcd_dvd_right i j), natAbs_ofNat, Nat.div_self H]
[GOAL]
i j : ℤ
H : j ∣ i
⊢ gcd i j = natAbs j
[PROOFSTEP]
rw [gcd_comm, gcd_eq_left H]
[GOAL]
x y : ℤ
hc : gcd x y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0
[PROOFSTEP]
contrapose! hc
[GOAL]
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ gcd x y = 0
[PROOFSTEP]
rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]
[GOAL]
m n : ℤ
k : ℕ
k0 : 0 < k
⊢ m ^ k ∣ n ^ k ↔ m ∣ n
[PROOFSTEP]
refine' ⟨fun h => _, fun h => pow_dvd_pow_of_dvd h _⟩
[GOAL]
m n : ℤ
k : ℕ
k0 : 0 < k
h : m ^ k ∣ n ^ k
⊢ m ∣ n
[PROOFSTEP]
rwa [← natAbs_dvd_natAbs, ← Nat.pow_dvd_pow_iff k0, ← Int.natAbs_pow, ← Int.natAbs_pow, natAbs_dvd_natAbs]
[GOAL]
a b : ℤ
n : ℕ
⊢ gcd a b ∣ n ↔ ∃ x y, ↑n = a * x + b * y
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
n : ℕ
⊢ gcd a b ∣ n → ∃ x y, ↑n = a * x + b * y
[PROOFSTEP]
intro h
[GOAL]
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y
[PROOFSTEP]
rw [← Nat.mul_div_cancel' h, Int.ofNat_mul, gcd_eq_gcd_ab, add_mul, mul_assoc, mul_assoc]
[GOAL]
case mp
a b : ℤ
n : ℕ
h : gcd a b ∣ n
⊢ ∃ x y, a * (gcdA a b * ↑(n / gcd a b)) + b * (gcdB a b * ↑(n / gcd a b)) = a * x + b * y
[PROOFSTEP]
exact ⟨_, _, rfl⟩
[GOAL]
case mpr
a b : ℤ
n : ℕ
⊢ (∃ x y, ↑n = a * x + b * y) → gcd a b ∣ n
[PROOFSTEP]
rintro ⟨x, y, h⟩
[GOAL]
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ gcd a b ∣ n
[PROOFSTEP]
rw [← Int.coe_nat_dvd, h]
[GOAL]
case mpr.intro.intro
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(gcd a b) ∣ a * x + b * y
[PROOFSTEP]
exact dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left a b) _) (dvd_mul_of_dvd_left (gcd_dvd_right a b) y)
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
⊢ a ∣ b
[PROOFSTEP]
have := gcd_eq_gcd_ab a c
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : ↑(gcd a c) = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
[PROOFSTEP]
simp only [hab, Int.ofNat_zero, Int.ofNat_succ, zero_add] at this
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : 1 = a * gcdA a c + c * gcdB a c
⊢ a ∣ b
[PROOFSTEP]
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← mul_add, ← this]
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this : 1 = a * gcdA a c + c * gcdB a c
⊢ b * a * gcdA a c + b * c * gcdB a c = b
[PROOFSTEP]
simp [mul_assoc, ← mul_add, ← this]
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b
[PROOFSTEP]
rw [← this]
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a c = 1
this✝ : 1 = a * gcdA a c + c * gcdB a c
this : b * a * gcdA a c + b * c * gcdB a c = b
⊢ a ∣ b * a * gcdA a c + b * c * gcdB a c
[PROOFSTEP]
exact dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b) _) (dvd_mul_of_dvd_left habc _)
[GOAL]
a b c : ℤ
habc : a ∣ b * c
hab : gcd a b = 1
⊢ a ∣ c
[PROOFSTEP]
rw [mul_comm] at habc
[GOAL]
a b c : ℤ
habc : a ∣ c * b
hab : gcd a b = 1
⊢ a ∣ c
[PROOFSTEP]
exact dvd_of_dvd_mul_left_of_gcd_one habc hab
[GOAL]
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (gcd a b)
[PROOFSTEP]
simp_rw [← gcd_dvd_iff]
[GOAL]
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ gcd a b ∣ n} (gcd a b)
[PROOFSTEP]
constructor
[GOAL]
case left
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ {n | 0 < n ∧ gcd a b ∣ n}
[PROOFSTEP]
simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
[GOAL]
case right
a b : ℤ
ha : a ≠ 0
⊢ gcd a b ∈ lowerBounds {n | 0 < n ∧ gcd a b ∣ n}
[PROOFSTEP]
simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
[GOAL]
case right
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → gcd a b ∣ a_1 → gcd a b ≤ a_1
[PROOFSTEP]
exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn
[GOAL]
i j : ℤ
⊢ lcm i j = lcm j i
[PROOFSTEP]
rw [Int.lcm, Int.lcm]
[GOAL]
i j : ℤ
⊢ Nat.lcm (natAbs i) (natAbs j) = Nat.lcm (natAbs j) (natAbs i)
[PROOFSTEP]
exact Nat.lcm_comm _ _
[GOAL]
i j k : ℤ
⊢ lcm (↑(lcm i j)) k = lcm i ↑(lcm j k)
[PROOFSTEP]
rw [Int.lcm, Int.lcm, Int.lcm, Int.lcm, natAbs_ofNat, natAbs_ofNat]
[GOAL]
i j k : ℤ
⊢ Nat.lcm (Nat.lcm (natAbs i) (natAbs j)) (natAbs k) = Nat.lcm (natAbs i) (Nat.lcm (natAbs j) (natAbs k))
[PROOFSTEP]
apply Nat.lcm_assoc
[GOAL]
i : ℤ
⊢ lcm 0 i = 0
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i : ℤ
⊢ Nat.lcm (natAbs 0) (natAbs i) = 0
[PROOFSTEP]
apply Nat.lcm_zero_left
[GOAL]
i : ℤ
⊢ lcm i 0 = 0
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i : ℤ
⊢ Nat.lcm (natAbs i) (natAbs 0) = 0
[PROOFSTEP]
apply Nat.lcm_zero_right
[GOAL]
i : ℤ
⊢ lcm 1 i = natAbs i
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i : ℤ
⊢ Nat.lcm (natAbs 1) (natAbs i) = natAbs i
[PROOFSTEP]
apply Nat.lcm_one_left
[GOAL]
i : ℤ
⊢ lcm i 1 = natAbs i
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i : ℤ
⊢ Nat.lcm (natAbs i) (natAbs 1) = natAbs i
[PROOFSTEP]
apply Nat.lcm_one_right
[GOAL]
i : ℤ
⊢ lcm i i = natAbs i
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i : ℤ
⊢ Nat.lcm (natAbs i) (natAbs i) = natAbs i
[PROOFSTEP]
apply Nat.lcm_self
[GOAL]
i j : ℤ
⊢ i ∣ ↑(lcm i j)
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i j : ℤ
⊢ i ∣ ↑(Nat.lcm (natAbs i) (natAbs j))
[PROOFSTEP]
apply coe_nat_dvd_right.mpr
[GOAL]
i j : ℤ
⊢ natAbs i ∣ Nat.lcm (natAbs i) (natAbs j)
[PROOFSTEP]
apply Nat.dvd_lcm_left
[GOAL]
i j : ℤ
⊢ j ∣ ↑(lcm i j)
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i j : ℤ
⊢ j ∣ ↑(Nat.lcm (natAbs i) (natAbs j))
[PROOFSTEP]
apply coe_nat_dvd_right.mpr
[GOAL]
i j : ℤ
⊢ natAbs j ∣ Nat.lcm (natAbs i) (natAbs j)
[PROOFSTEP]
apply Nat.dvd_lcm_right
[GOAL]
i j k : ℤ
⊢ i ∣ k → j ∣ k → ↑(lcm i j) ∣ k
[PROOFSTEP]
rw [Int.lcm]
[GOAL]
i j k : ℤ
⊢ i ∣ k → j ∣ k → ↑(Nat.lcm (natAbs i) (natAbs j)) ∣ k
[PROOFSTEP]
intro hi hj
[GOAL]
i j k : ℤ
hi : i ∣ k
hj : j ∣ k
⊢ ↑(Nat.lcm (natAbs i) (natAbs j)) ∣ k
[PROOFSTEP]
exact coe_nat_dvd_left.mpr (Nat.lcm_dvd (natAbs_dvd_natAbs.mpr hi) (natAbs_dvd_natAbs.mpr hj))
[GOAL]
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
hm : x ^ m = 1
hn : x ^ n = 1
⊢ x ^ Nat.gcd m n = 1
[PROOFSTEP]
rcases m with (rfl | m)
[GOAL]
case zero
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
hm : x ^ Nat.zero = 1
⊢ x ^ Nat.gcd Nat.zero n = 1
[PROOFSTEP]
simp [hn]
[GOAL]
case succ
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
m : ℕ
hm : x ^ Nat.succ m = 1
⊢ x ^ Nat.gcd (Nat.succ m) n = 1
[PROOFSTEP]
obtain ⟨y, rfl⟩ := isUnit_ofPowEqOne hm m.succ_ne_zero
[GOAL]
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑y ^ n = 1
hm : ↑y ^ Nat.succ m = 1
⊢ ↑y ^ Nat.gcd (Nat.succ m) n = 1
[PROOFSTEP]
simp only [← Units.val_pow_eq_pow_val] at *
[GOAL]
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑(y ^ n) = 1
hm : ↑(y ^ Nat.succ m) = 1
⊢ ↑(y ^ Nat.gcd (Nat.succ m) n) = 1
[PROOFSTEP]
rw [← Units.val_one, ← zpow_coe_nat, ← Units.ext_iff] at *
[GOAL]
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(Nat.succ m) = 1
⊢ y ^ ↑(Nat.gcd (Nat.succ m) n) = 1
[PROOFSTEP]
simp only [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, hm, hn, one_zpow, one_mul]


[GOAL]
μ : YoungDiagram
T T' : Ssyt μ
h : T.entry = T'.entry
⊢ T = T'
[PROOFSTEP]
cases T
[GOAL]
case mk
μ : YoungDiagram
T' : Ssyt μ
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝ i j = 0
h : { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry = T'.entry
⊢ { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ } = T'
[PROOFSTEP]
cases T'
[GOAL]
case mk.mk
μ : YoungDiagram
entry✝¹ : ℕ → ℕ → ℕ
row_weak'✝¹ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝¹ i j1 ≤ entry✝¹ i j2
col_strict'✝¹ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝¹ i1 j < entry✝¹ i2 j
zeros'✝¹ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝¹ i j = 0
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝ i j = 0
h :
  { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ }.entry =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry
⊢ { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ } =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }
[PROOFSTEP]
congr
[GOAL]
μ : YoungDiagram
T T' : Ssyt μ
h : ∀ (i j : ℕ), ↑T i j = ↑T' i j
x✝ : ℕ
⊢ ↑T x✝ = ↑T' x✝
[PROOFSTEP]
funext
[GOAL]
case h
μ : YoungDiagram
T T' : Ssyt μ
h : ∀ (i j : ℕ), ↑T i j = ↑T' i j
x✝¹ x✝ : ℕ
⊢ ↑T x✝¹ x✝ = ↑T' x✝¹ x✝
[PROOFSTEP]
apply h
[GOAL]
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
cases' eq_or_lt_of_le hj with h h
[GOAL]
case inl
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
rw [h]
[GOAL]
case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
exact T.row_weak h cell
[GOAL]
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
cases' eq_or_lt_of_le hi with h h
[GOAL]
case inl
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
rw [h]
[GOAL]
case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
exact le_of_lt (T.col_strict h cell)
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (fun i j => if (i, j) ∈ μ then i else 0) i✝ j1✝ ≤ (fun i j => if (i, j) ∈ μ then i else 0) i✝ j2✝
[PROOFSTEP]
simp only
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (if (i✝, j1✝) ∈ μ then i✝ else 0) ≤ if (i✝, j2✝) ∈ μ then i✝ else 0
[PROOFSTEP]
rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ i✝ ≤ i✝
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ (fun i j => if (i, j) ∈ μ then i else 0) i1✝ j✝ < (fun i j => if (i, j) ∈ μ then i else 0) i2✝ j✝
[PROOFSTEP]
simp only
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ (if (i1✝, j✝) ∈ μ then i1✝ else 0) < if (i2✝, j✝) ∈ μ then i2✝ else 0
[PROOFSTEP]
rwa [if_pos hcell, if_pos (μ.up_left_mem (le_of_lt hi) (by rfl) hcell)]
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ j✝ ≤ j✝
[PROOFSTEP]
rfl


[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
⊢ Injective fun f => φ.map f
[PROOFSTEP]
rintro f g he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ f = g
[PROOFSTEP]
have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ star φ u (Star.mk f) = star φ u (Star.mk g)
[PROOFSTEP]
simpa using he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
this : star φ u (Star.mk f) = star φ u (Star.mk g)
⊢ f = g
[PROOFSTEP]
simpa using (hφ.star_bijective u).left this
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
⊢ Prefunctor.IsCovering ψ
[PROOFSTEP]
refine' ⟨fun v => _, fun v => _⟩
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
v : V
⊢ Bijective (star ψ v)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := φsur v
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
v : V
⊢ Bijective (costar ψ v)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := φsur v
[GOAL]
case refine'_1.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
u : U
⊢ Bijective (star ψ (φ.obj u))
case refine'_2.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
u : U
⊢ Bijective (costar ψ (φ.obj u))
[PROOFSTEP]
exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
  (Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ star (symmetrify φ) u =
    ↑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)
[PROOFSTEP]
rw [Equiv.eq_symm_comp]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ ↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u =
    Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)
[PROOFSTEP]
ext ⟨v, f | g⟩
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u) { fst := v, snd := Sum.inl f } =
    (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)) { fst := v, snd := Sum.inl f }
[PROOFSTEP]
simp only [Quiver.symmetrifyStar, Function.comp_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u) { fst := v, snd := Sum.inr g } =
    (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)) { fst := v, snd := Sum.inr g }
[PROOFSTEP]
simp only [Quiver.symmetrifyStar, Function.comp_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ ↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj (φ.obj u) ⟶ v) fun v => v ⟶ Symmetrify.of.obj (φ.obj u))
      (star (symmetrify φ) u { fst := v, snd := Sum.inl f }) =
    Sum.map (star φ u) (costar φ u)
      (↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj u ⟶ v) fun v => v ⟶ Symmetrify.of.obj u)
        { fst := v, snd := Sum.inl f })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ ↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj (φ.obj u) ⟶ v) fun v => v ⟶ Symmetrify.of.obj (φ.obj u))
      (star (symmetrify φ) u { fst := v, snd := Sum.inr g }) =
    Sum.map (star φ u) (costar φ u)
      (↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj u ⟶ v) fun v => v ⟶ Symmetrify.of.obj u)
        { fst := v, snd := Sum.inr g })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).snd =
    Sum.map (star φ u) (costar φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inl f }.fst) (Sigma.mk { fst := v, snd := Sum.inl f }.fst)
        { fst := v, snd := Sum.inl f }.snd)
[PROOFSTEP]
simp
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).snd =
    Sum.map (star φ u) (costar φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inr g }.fst) (Sigma.mk { fst := v, snd := Sum.inr g }.fst)
        { fst := v, snd := Sum.inr g }.snd)
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ costar (symmetrify φ) u = ↑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)
[PROOFSTEP]
rw [Equiv.eq_symm_comp]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ ↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u = Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)
[PROOFSTEP]
ext ⟨v, f | g⟩
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u) { fst := v, snd := Sum.inl f } =
    (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)) { fst := v, snd := Sum.inl f }
[PROOFSTEP]
simp only [Quiver.symmetrifyCostar, Function.comp_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u) { fst := v, snd := Sum.inr g } =
    (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)) { fst := v, snd := Sum.inr g }
[PROOFSTEP]
simp only [Quiver.symmetrifyCostar, Function.comp_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ ↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj (φ.obj u)) fun u_1 => Symmetrify.of.obj (φ.obj u) ⟶ u_1)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }) =
    Sum.map (costar φ u) (star φ u)
      (↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj u) fun u_1 => Symmetrify.of.obj u ⟶ u_1)
        { fst := v, snd := Sum.inl f })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ ↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj (φ.obj u)) fun u_1 => Symmetrify.of.obj (φ.obj u) ⟶ u_1)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }) =
    Sum.map (costar φ u) (star φ u)
      (↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj u) fun u_1 => Symmetrify.of.obj u ⟶ u_1)
        { fst := v, snd := Sum.inr g })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).snd =
    Sum.map (costar φ u) (star φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inl f }.fst) (Sigma.mk { fst := v, snd := Sum.inl f }.fst)
        { fst := v, snd := Sum.inl f }.snd)
[PROOFSTEP]
simp
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).snd =
    Sum.map (costar φ u) (star φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inr g }.fst) (Sigma.mk { fst := v, snd := Sum.inr g }.fst)
        { fst := v, snd := Sum.inr g }.snd)
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
⊢ Prefunctor.IsCovering (symmetrify φ)
[PROOFSTEP]
refine' ⟨fun u => _, fun u => _⟩
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (star (symmetrify φ) u)
[PROOFSTEP]
simp only [φ.symmetrifyStar, φ.symmetrifyCostar, EquivLike.comp_bijective]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (costar (symmetrify φ) u)
[PROOFSTEP]
simp only [φ.symmetrifyStar, φ.symmetrifyCostar, EquivLike.comp_bijective]
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u))
[PROOFSTEP]
erw [EquivLike.bijective_comp]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u))
[PROOFSTEP]
erw [EquivLike.bijective_comp]
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (star φ u) (costar φ u))
[PROOFSTEP]
simp [hφ.star_bijective u, hφ.costar_bijective u]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (costar φ u) (star φ u))
[PROOFSTEP]
simp [hφ.star_bijective u, hφ.costar_bijective u]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u : U
⊢ Injective (pathStar φ u)
[PROOFSTEP]
dsimp [Prefunctor.pathStar, Quiver.PathStar.mk]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u : U
⊢ Injective fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }
[PROOFSTEP]
rintro ⟨v₁, p₁⟩
[GOAL]
case mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
p₁ : Path u v₁
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := v₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := v₁, snd := p₁ } = a₂
[PROOFSTEP]
induction' p₁ with x₁ y₁ p₁ e₁ ih
[GOAL]
case mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := u, snd := Path.nil } = a₂
[PROOFSTEP]
rintro ⟨y₂, p₂⟩
[GOAL]
case mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := y₁, snd := Path.cons p₁ e₁ } = a₂
[PROOFSTEP]
rintro ⟨y₂, p₂⟩
[GOAL]
case mk.nil.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ : U
p₂ : Path u y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := p₂ } →
    { fst := u, snd := Path.nil } = { fst := y₂, snd := p₂ }
[PROOFSTEP]
cases' p₂ with x₂ _ p₂ e₂
[GOAL]
case mk.cons.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
p₂ : Path u y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := p₂ } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := p₂ }
[PROOFSTEP]
cases' p₂ with x₂ _ p₂ e₂
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } →
    { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
intro h
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ } →
    { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
intro h
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
intro h
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
intro h
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil }
⊢ { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ }
⊢ { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
h : True
⊢ { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
rfl
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
exfalso
[GOAL]
case mk.nil.mk.cons.h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ False
[PROOFSTEP]
cases' h with h h'
[GOAL]
case mk.nil.mk.cons.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ False
[PROOFSTEP]
rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
[GOAL]
case mk.nil.mk.cons.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' :
  Path.nil =
    Path.cons (Path.cast (_ : φ.obj u = φ.obj u) (_ : φ.obj x₂ = φ.obj x₂) (mapPath φ p₂))
      (Hom.cast (_ : φ.obj x₂ = φ.obj x₂) (_ : φ.obj y₂ = φ.obj u) (φ.map e₂))
⊢ False
[PROOFSTEP]
exact (Path.nil_ne_cons _ _) h'
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
exfalso
[GOAL]
case mk.cons.mk.nil.h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ False
[PROOFSTEP]
cases' h with h h'
[GOAL]
case mk.cons.mk.nil.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u
h' : HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ False
[PROOFSTEP]
rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
[GOAL]
case mk.cons.mk.nil.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u
h' :
  Path.cons (Path.cast (_ : φ.obj u = φ.obj u) (_ : φ.obj x₁ = φ.obj x₁) (mapPath φ p₁))
      (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) h (φ.map e₁)) =
    Path.nil
⊢ False
[PROOFSTEP]
exact (Path.cons_ne_nil _ _) h'
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj y₁ = φ.obj y₂ ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
cases' h with hφy h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφx := Path.obj_eq_of_cons_eq_cons h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφp := Path.heq_of_cons_eq_cons h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
  simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₂, snd := p₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ φ.obj x₁ = φ.obj x₂ ∧ HEq (mapPath φ p₁) (mapPath φ p₂)
[PROOFSTEP]
exact ⟨hφx, hφp⟩
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₂, snd := p₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
cases ih h_path_star
[GOAL]
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₁ e₂ }
[PROOFSTEP]
have h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩ := by simp only [Prefunctor.star_apply, Sigma.mk.inj_iff];
  exact ⟨hφy, hφe⟩
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₂, snd := e₂ }
[PROOFSTEP]
simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ φ.obj y₁ = φ.obj y₂ ∧ HEq (φ.map e₁) (φ.map e₂)
[PROOFSTEP]
exact ⟨hφy, hφe⟩
[GOAL]
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
h_star : star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₂, snd := e₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₁ e₂ }
[PROOFSTEP]
cases hφ x₁ h_star
[GOAL]
case mk.cons.mk.cons.intro.refl.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
hφx : φ.obj x₁ = φ.obj x₁
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
hφy : φ.obj y₁ = φ.obj y₁
hφe : HEq (φ.map e₁) (φ.map e₁)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₁)
h_star : star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₁, snd := e₁ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₁, snd := Path.cons p₁ e₁ }
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
⊢ Surjective (pathStar φ u)
[PROOFSTEP]
dsimp [Prefunctor.pathStar, Quiver.PathStar.mk]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
⊢ Surjective fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }
[PROOFSTEP]
rintro ⟨v, p⟩
[GOAL]
case mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
p : Path (φ.obj u) v
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v, snd := p }
[PROOFSTEP]
induction' p with v' v'' p' ev ih
[GOAL]
case mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := φ.obj u, snd := Path.nil }
[PROOFSTEP]
use⟨u, Path.nil⟩
[GOAL]
case h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    { fst := φ.obj u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.mapPath_nil, eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
case mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
ih : ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
obtain ⟨⟨u', q'⟩, h⟩ := ih
[GOAL]
case mk.cons.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
u' : U
q' : Path u u'
h : (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u', snd := q' } = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
simp only at h
[GOAL]
case mk.cons.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
u' : U
q' : Path u u'
h : { fst := φ.obj u', snd := mapPath φ q' } = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := h
[GOAL]
case mk.cons.intro.mk.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
[GOAL]
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
u'' : U
eu : u' ⟶ u''
k : star φ u' { fst := u'', snd := eu } = { fst := v'', snd := ev }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
simp only [star_apply, Sigma.mk.inj_iff] at k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = v'' ∧ HEq (φ.map eu) ev
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
obtain ⟨rfl, k⟩ := k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : HEq (φ.map eu) ev
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
simp only [heq_eq_eq] at k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu = ev
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
subst k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') (φ.map eu) }
[PROOFSTEP]
use⟨_, q'.cons eu⟩
[GOAL]
case h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u'', snd := Path.cons q' eu } =
    { fst := φ.obj u'', snd := Path.cons (mapPath φ q') (φ.map eu) }
[PROOFSTEP]
simp only [Prefunctor.mapPath_cons, eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
U : Type ?u.18936
inst✝⁵ : Quiver U
V : Type ?u.18942
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.18964
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : Prefunctor.MapReverse φ
u : U
e : Star u
⊢ (fun e => { fst := e.fst, snd := reverse e.snd }) ((fun e => { fst := e.fst, snd := reverse e.snd }) e) = e
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
U : Type ?u.18936
inst✝⁵ : Quiver U
V : Type ?u.18942
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.18964
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : Prefunctor.MapReverse φ
u : U
e : Costar u
⊢ (fun e => { fst := e.fst, snd := reverse e.snd }) ((fun e => { fst := e.fst, snd := reverse e.snd }) e) = e
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u : U
⊢ costar φ u = ↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm
[PROOFSTEP]
ext ⟨v, f⟩
[GOAL]
case h.mk.h₀
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u v : U
f : v ⟶ u
⊢ (costar φ u { fst := v, snd := f }).fst =
    ((↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm) { fst := v, snd := f }).fst
[PROOFSTEP]
simp
[GOAL]
case h.mk.h₁
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u v : U
f : v ⟶ u
⊢ HEq (costar φ u { fst := v, snd := f }).snd
    ((↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm) { fst := v, snd := f }).snd
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.22299
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u : U
⊢ Bijective (costar φ u) ↔ Bijective (star φ u)
[PROOFSTEP]
rw [Prefunctor.costar_conj_star, EquivLike.comp_bijective, EquivLike.bijective_comp]


[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases show ∃ n, height b < n from ⟨_, Nat.lt.base _⟩ with ⟨n, hn⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
n : ℕ
hn : height b < n
⊢ Nonempty (Path r b)
[PROOFSTEP]
induction' n with n ih generalizing b
[GOAL]
case intro.zero
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n : ℕ
hn✝ : height b✝ < n
b : V
hn : height b < Nat.zero
⊢ Nonempty (Path r b)
[PROOFSTEP]
exact False.elim (Nat.not_lt_zero _ hn)
[GOAL]
case intro.succ
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases root_or_arrow b with (⟨⟨⟩⟩ | ⟨a, ⟨e⟩⟩)
[GOAL]
case intro.succ.inl.refl
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
n✝ : ℕ
hn✝ : height b < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
hn : height r < Nat.succ n
⊢ Nonempty (Path r r)
[PROOFSTEP]
exact ⟨Path.nil⟩
[GOAL]
case intro.succ.inr.intro.intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
a : V
e : a ⟶ b
⊢ Nonempty (Path r b)
[PROOFSTEP]
rcases ih a (lt_of_lt_of_le (height_lt e) (Nat.lt_succ_iff.mp hn)) with ⟨p⟩
[GOAL]
case intro.succ.inr.intro.intro.intro
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
n✝ : ℕ
hn✝ : height b✝ < n✝
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < Nat.succ n
a : V
e : a ⟶ b
p : Path r a
⊢ Nonempty (Path r b)
[PROOFSTEP]
exact ⟨p.cons e⟩
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
have height_le : ∀ {a b}, Path a b → height a ≤ height b :=
  by
  intro a b p
  induction' p with b c _ e ih
  rfl
  exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ ∀ {a b : V}, Path a b → height a ≤ height b
[PROOFSTEP]
intro a b p
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ a b : V
p : Path a b
⊢ height a ≤ height b
[PROOFSTEP]
induction' p with b c _ e ih
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ a b : V
⊢ height a ≤ height a
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝¹ a b✝ b c : V
a✝ : Path a b
e : b ⟶ c
ih : height a ≤ height b
⊢ height a ≤ height c
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝¹ a b✝ b c : V
a✝ : Path a b
e : b ⟶ c
ih : height a ≤ height b
⊢ height a ≤ height c
[PROOFSTEP]
exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
suffices ∀ p q : Path r b, p = q by
  intro p
  apply this
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
this : ∀ (p q : Path r b), p = q
⊢ ∀ (a : Path r b), a = default
[PROOFSTEP]
intro p
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
this : ∀ (p q : Path r b), p = q
p : Path r b
⊢ p = default
[PROOFSTEP]
apply this
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
⊢ ∀ (p q : Path r b), p = q
[PROOFSTEP]
intro p q
[GOAL]
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
p q : Path r b
⊢ p = q
[PROOFSTEP]
induction' p with a c p e ih
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
q : Path r r
⊢ Path.nil = q
[PROOFSTEP]
cases' q with b _ q f
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
q : Path r c
⊢ Path.cons p e = q
[PROOFSTEP]
cases' q with b _ q f
[GOAL]
case nil.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q : Path r b
⊢ Path.nil = Path.nil
[PROOFSTEP]
rfl
[GOAL]
case nil.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b✝
b : V
q : Path r b
f : b ⟶ r
⊢ Path.nil = Path.cons q f
[PROOFSTEP]
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))
[GOAL]
case cons.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q : Path r b
a : V
p : Path r a
ih : ∀ (q : Path r a), p = q
e : a ⟶ r
⊢ Path.cons p e = Path.nil
[PROOFSTEP]
exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))
[GOAL]
case cons.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b✝
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
b : V
q : Path r b
f : b ⟶ c
⊢ Path.cons p e = Path.cons q f
[PROOFSTEP]
rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
[GOAL]
case cons.cons.intro.refl.refl
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄, (a ⟶ b) → height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V}, Path a b → height a ≤ height b
q✝ : Path r b
a c : V
p : Path r a
e : a ⟶ c
ih : ∀ (q : Path r a), p = q
q : Path r a
β : Sort ?u.237
⊢ Path.cons p e = Path.cons q e
[PROOFSTEP]
rw [ih]
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b : WideSubquiver.toType V (geodesicSubtree r)⦄,
    (a ⟶ b) → (fun a => Path.length (shortestPath r a)) a < (fun a => Path.length (shortestPath r a)) b
[PROOFSTEP]
rintro a b ⟨e, p, h⟩
[GOAL]
case mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = Path.cons p e
⊢ (fun a => Path.length (shortestPath r a)) a < (fun a => Path.length (shortestPath r a)) b
[PROOFSTEP]
simp_rw [h, Path.length_cons, Nat.lt_succ_iff]
[GOAL]
case mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ b
p : Path r a
h : shortestPath r b = Path.cons p e
⊢ Path.length (shortestPath r a) ≤ Path.length p
[PROOFSTEP]
apply shortest_path_spec
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ ⦃a b c : WideSubquiver.toType V (geodesicSubtree r)⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ HEq e f
[PROOFSTEP]
rintro a b c ⟨e, p, h⟩ ⟨f, q, j⟩
[GOAL]
case mk.intro.mk.intro
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a b c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h : shortestPath r c = Path.cons p e
f : b ⟶ c
q : Path r b
j : shortestPath r c = Path.cons q f
⊢ a = b ∧
    HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
      { val := f, property := (_ : ∃ p, shortestPath r c = Path.cons p f) }
[PROOFSTEP]
cases h.symm.trans j
[GOAL]
case mk.intro.mk.intro.refl
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ a = a ∧
    HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
      { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.mk.intro.refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case mk.intro.mk.intro.refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = Path.cons p e
⊢ HEq { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
    { val := e, property := (_ : ∃ p, shortestPath r c = Path.cons p e) }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ (b : WideSubquiver.toType V (geodesicSubtree r)), b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
intro b
[GOAL]
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
rcases hp : shortestPath r b with (_ | ⟨p, e⟩)
[GOAL]
case nil
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
hp : shortestPath r r = Path.nil
⊢ r = r ∨ ∃ a, Nonempty (a ⟶ r)
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case cons
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
b✝ : V
p : Path r b✝
e : b✝ ⟶ b
hp : shortestPath r b = Path.cons p e
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
[PROOFSTEP]
exact Or.inr ⟨_, ⟨⟨e, p, hp⟩⟩⟩


[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
e : b ⟶ a
h : nil = cons p e
⊢ False
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
e : b ⟶ a
h : cons p e = nil
⊢ False
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : cons p e = cons p' e'
⊢ b = c
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : cons p e = cons p' e'
⊢ HEq p p'
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : cons p e = cons p' e'
⊢ HEq e e'
[PROOFSTEP]
injection h
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
hzero : length p = 0
⊢ a = b
[PROOFSTEP]
cases p
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
a c d : V
hzero : length nil = 0
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
a b c d b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : length (cons a✝¹ a✝) = 0
⊢ a = b
[PROOFSTEP]
cases Nat.succ_ne_zero _ hzero
[GOAL]
V : Type u
inst✝ : Quiver V
a✝¹ b c d a x✝ b✝ : V
p : Path a b✝
a✝ : b✝ ⟶ x✝
⊢ comp nil (cons p a✝) = cons p a✝
[PROOFSTEP]
rw [comp_cons, nil_comp p]
[GOAL]
V : Type u
inst✝ : Quiver V
a✝¹ b✝¹ c✝ d a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
[PROOFSTEP]
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : length q₁ = length q₂
⊢ comp p₁ q₁ = comp p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
[PROOFSTEP]
refine' ⟨fun h => _, by rintro ⟨rfl, rfl⟩; rfl⟩
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : length q₁ = length q₂
⊢ p₁ = p₂ ∧ q₁ = q₂ → comp p₁ q₁ = comp p₂ q₂
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
hq : length q₁ = length q₁
⊢ comp p₁ q₁ = comp p₁ q₁
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq : length q₁ = length q₂
h : comp p₁ q₁ = comp p₂ q₂
⊢ p₁ = p₂ ∧ q₁ = q₂
[PROOFSTEP]
induction' q₁ with d₁ e₁ q₁ f₁ ih
[GOAL]
case nil
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂✝ : Path b c
hq✝ : length q₁ = length q₂✝
h✝ : comp p₁ q₁ = comp p₂ q₂✝
q₂ : Path b b
hq : length nil = length q₂
h : comp p₁ nil = comp p₂ q₂
⊢ p₁ = p₂ ∧ nil = q₂
[PROOFSTEP]
obtain _ | ⟨q₂, f₂⟩ := q₂
[GOAL]
case cons
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁✝ q₂✝ : Path b c
hq✝ : length q₁✝ = length q₂✝
h✝ : comp p₁ q₁✝ = comp p₂ q₂✝
d₁ e₁ : V
q₁ : Path b d₁
f₁ : d₁ ⟶ e₁
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₂ q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b e₁
hq : length (cons q₁ f₁) = length q₂
h : comp p₁ (cons q₁ f₁) = comp p₂ q₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = q₂
[PROOFSTEP]
obtain _ | ⟨q₂, f₂⟩ := q₂
[GOAL]
case nil.nil
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
hq✝ : length q₁ = length q₂
h✝ : comp p₁ q₁ = comp p₂ q₂
hq : length nil = length nil
h : comp p₁ nil = comp p₂ nil
⊢ p₁ = p₂ ∧ nil = nil
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
case nil.cons
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂✝ : Path b c
hq✝ : length q₁ = length q₂✝
h✝ : comp p₁ q₁ = comp p₂ q₂✝
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : length nil = length (cons q₂ f₂)
h : comp p₁ nil = comp p₂ (cons q₂ f₂)
⊢ p₁ = p₂ ∧ nil = cons q₂ f₂
[PROOFSTEP]
cases hq
[GOAL]
case cons.nil
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁✝ q₂ : Path b c
hq✝ : length q₁✝ = length q₂
h✝ : comp p₁ q₁✝ = comp p₂ q₂
d₁ : V
q₁ : Path b d₁
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₂ q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : d₁ ⟶ b
hq : length (cons q₁ f₁) = length nil
h : comp p₁ (cons q₁ f₁) = comp p₂ nil
⊢ p₁ = p₂ ∧ cons q₁ f₁ = nil
[PROOFSTEP]
cases hq
[GOAL]
case cons.cons
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁✝ q₂✝ : Path b c
hq✝ : length q₁✝ = length q₂✝
h✝ : comp p₁ q₁✝ = comp p₂ q₂✝
d₁ e₁ : V
q₁ : Path b d₁
f₁ : d₁ ⟶ e₁
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₂ q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ e₁
hq : length (cons q₁ f₁) = length (cons q₂ f₂)
h : comp p₁ (cons q₁ f₁) = comp p₂ (cons q₂ f₂)
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
simp only [comp_cons, cons.injEq] at h
[GOAL]
case cons.cons
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁✝ q₂✝ : Path b c
hq✝ : length q₁✝ = length q₂✝
h✝ : comp p₁ q₁✝ = comp p₂ q₂✝
d₁ e₁ : V
q₁ : Path b d₁
f₁ : d₁ ⟶ e₁
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₂ q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ e₁
hq : length (cons q₁ f₁) = length (cons q₂ f₂)
h : d₁ = b✝ ∧ HEq (comp p₁ q₁) (comp p₂ q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
obtain rfl := h.1
[GOAL]
case cons.cons
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁✝ q₂✝ : Path b c
hq✝ : length q₁✝ = length q₂✝
h✝ : comp p₁ q₁✝ = comp p₂ q₂✝
d₁ e₁ : V
q₁ : Path b d₁
f₁ : d₁ ⟶ e₁
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₂ q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b d₁
f₂ : d₁ ⟶ e₁
hq : length (cons q₁ f₁) = length (cons q₂ f₂)
h : d₁ = d₁ ∧ HEq (comp p₁ q₁) (comp p₂ q₂) ∧ HEq f₁ f₂
⊢ p₁ = p₂ ∧ cons q₁ f₁ = cons q₂ f₂
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
[GOAL]
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁✝ q₂ : Path b c
hq✝ : length q₁✝ = length q₂
d₁ e₁ : V
q₁ : Path b d₁
f₁ f₂ : d₁ ⟶ e₁
h✝ : comp p₁ q₁✝ = comp p₁ q₂
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₁ q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : length (cons q₁ f₁) = length (cons q₁ f₂)
h : d₁ = d₁ ∧ HEq (comp p₁ q₁) (comp p₁ q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ cons q₁ f₁ = cons q₁ f₂
[PROOFSTEP]
rw [h.2.2.eq]
[GOAL]
case cons.cons.intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁✝ q₂ : Path b c
hq✝ : length q₁✝ = length q₂
d₁ e₁ : V
q₁ : Path b d₁
f₁ f₂ : d₁ ⟶ e₁
h✝ : comp p₁ q₁✝ = comp p₁ q₂
ih : ∀ {q₂ : Path b d₁}, length q₁ = length q₂ → comp p₁ q₁ = comp p₁ q₂ → p₁ = p₁ ∧ q₁ = q₂
hq : length (cons q₁ f₁) = length (cons q₁ f₂)
h : d₁ = d₁ ∧ HEq (comp p₁ q₁) (comp p₁ q₁) ∧ HEq f₁ f₂
⊢ p₁ = p₁ ∧ cons q₁ f₂ = cons q₁ f₂
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : length p₁ = length p₂
h_eq : comp p₁ q₁ = comp p₂ q₂
⊢ ?m.8816 h h_eq + length q₁ = ?m.8816 h h_eq + length q₂
[PROOFSTEP]
simpa [h] using congr_arg length h_eq
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : length p₁ = length p₂
⊢ p₁ = p₂ ∧ q₁ = q₂ → comp p₁ q₁ = comp p₂ q₂
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
V : Type u
inst✝ : Quiver V
a b c d : V
p₁ : Path a b
q₁ : Path b c
h : length p₁ = length p₁
⊢ comp p₁ q₁ = comp p₁ q₁
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
⊢ toList (comp p nil) = toList nil ++ toList p
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝ : Quiver V
a b c d✝ : V
p : Path a b
x✝ d : V
q : Path b d
a✝ : d ⟶ x✝
⊢ toList (comp p (cons q a✝)) = toList (cons q a✝) ++ toList p
[PROOFSTEP]
simp [toList_comp]
[GOAL]
V : Type u
inst✝¹ : Quiver V
a✝ b c✝ d : V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : toList nil = toList (cons p f)
⊢ nil = cons p f
[PROOFSTEP]
cases h
[GOAL]
V : Type u
inst✝¹ : Quiver V
a✝ b c✝ d : V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : toList (cons p f) = toList nil
⊢ cons p f = nil
[PROOFSTEP]
cases h
[GOAL]
V : Type u
inst✝¹ : Quiver V
a✝ b c✝ d : V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : toList (cons p f) = toList (cons C D)
⊢ cons p f = cons C D
[PROOFSTEP]
simp only [toList, List.cons.injEq] at h
[GOAL]
V : Type u
inst✝¹ : Quiver V
a✝ b c✝ d : V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : c = t ∧ toList p = toList C
⊢ cons p f = cons C D
[PROOFSTEP]
obtain ⟨rfl, hAC⟩ := h
[GOAL]
case intro
V : Type u
inst✝¹ : Quiver V
a✝ b c✝ d : V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
C : Path a c
D : c ⟶ x✝
hAC : toList p = toList C
⊢ cons p f = cons C D
[PROOFSTEP]
simp [toList_injective _ _ hAC]
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ mapPath F (Path.comp p (Path.cons q e)) = Path.comp (mapPath F p) (mapPath F (Path.cons q e))
[PROOFSTEP]
dsimp
[GOAL]
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ Path.cons (mapPath F (Path.comp p q)) (F.map e) = Path.cons (Path.comp (mapPath F p) (mapPath F q)) (F.map e)
[PROOFSTEP]
rw [mapPath_comp p q]