[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
f g : (Fin n → G) → CoeSort.coe A
⊢ (fun f g =>
        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
          Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
      (f + g) =
    (fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
        f +
      (fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
        g
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
f g : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ (fun f g =>
        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
          Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
      (f + g) x =
    ((fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
          f +
        (fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
          g)
      x
[PROOFSTEP]
simp_rw [Pi.add_apply, map_add, smul_add, Finset.sum_add_distrib, add_add_add_comm]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
r : k
f : (Fin n → G) → CoeSort.coe A
⊢ AddHom.toFun
      {
        toFun := fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
        map_add' :=
          (_ :
            ∀ (f g : (Fin n → G) → CoeSort.coe A),
              (fun f g =>
                    ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                  (f + g) =
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    f +
                  (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    g) }
      (r • f) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        {
          toFun := fun f g =>
            ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
              Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
          map_add' :=
            (_ :
              ∀ (f g : (Fin n → G) → CoeSort.coe A),
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    (f + g) =
                  (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      f +
                    (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      g) }
        f
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
n : ℕ
A : Rep k G
r : k
f : (Fin n → G) → CoeSort.coe A
x : Fin (n + 1) → G
⊢ AddHom.toFun
      {
        toFun := fun f g =>
          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
            Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
        map_add' :=
          (_ :
            ∀ (f g : (Fin n → G) → CoeSort.coe A),
              (fun f g =>
                    ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                  (f + g) =
                (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    f +
                  (fun f g =>
                      ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                        Finset.sum Finset.univ fun j =>
                          (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                    g) }
      (r • f) x =
    (↑(RingHom.id k) r •
        AddHom.toFun
          {
            toFun := fun f g =>
              ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g),
            map_add' :=
              (_ :
                ∀ (f g : (Fin n → G) → CoeSort.coe A),
                  (fun f g =>
                        ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                          Finset.sum Finset.univ fun j =>
                            (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                      (f + g) =
                    (fun f g =>
                          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                            Finset.sum Finset.univ fun j =>
                              (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                        f +
                      (fun f g =>
                          ↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
                            Finset.sum Finset.univ fun j =>
                              (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g))
                        g) }
          f)
      x
[PROOFSTEP]
simp_rw [Pi.smul_apply, RingHom.id_apply, map_smul, smul_add, Finset.smul_sum, ← smul_assoc, smul_eq_mul, mul_comm r]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ d n A =
    (LinearEquiv.toModuleIso (diagonalHomEquiv n A)).inv ≫
      HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
        (LinearEquiv.toModuleIso (diagonalHomEquiv (n + 1) A)).hom
[PROOFSTEP]
ext f g
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑((LinearEquiv.toModuleIso (diagonalHomEquiv n A)).inv ≫
          HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
            (LinearEquiv.toModuleIso (diagonalHomEquiv (n + 1) A)).hom)
      f g
[PROOFSTEP]
change d n A f g = diagonalHomEquiv (n + 1) A ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(diagonalHomEquiv (n + 1) A)
      (HomologicalComplex.d (resolution k G) (n + 1) n ≫ ↑(LinearEquiv.symm (diagonalHomEquiv n A)) f) g
[PROOFSTEP]
rw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, Resolution.d_eq]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      (↑(Resolution.d k G (n + 1)) (Finsupp.single (Fin.partialProd g) 1))
[PROOFSTEP]
erw [Resolution.d_of (Fin.partialProd g)]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      (Finset.sum Finset.univ fun p => Finsupp.single (Fin.partialProd g ∘ Fin.succAbove p) ((-1) ^ ↑p))
[PROOFSTEP]
rw [LinearMap.map_sum]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    Finset.sum Finset.univ fun i =>
      ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
        (Finsupp.single (Fin.partialProd g ∘ Fin.succAbove i) ((-1) ^ ↑i))
[PROOFSTEP]
simp only [← Finsupp.smul_single_one _ ((-1 : k) ^ _)]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ ↑(d n A) f g =
    Finset.sum Finset.univ fun x =>
      ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
        ((-1) ^ ↑x • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove x) 1)
[PROOFSTEP]
rw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero,
  diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ (↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g)) =
    ↑(↑(ρ A) ((Fin.partialProd g ∘ Fin.succ) 0))
        (f fun i => ((Fin.partialProd g ∘ Fin.succ) (Fin.castSucc i))⁻¹ * (Fin.partialProd g ∘ Fin.succ) (Fin.succ i)) +
      Finset.sum Finset.univ fun i =>
        ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
          ((-1) ^ ↑(Fin.succ i) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ i)) 1)
[PROOFSTEP]
simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero, Fin.partialProd_zero, one_mul]
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
⊢ (↑(↑(ρ A) (g 0)) (f fun i => g (Fin.succ i)) +
      Finset.sum Finset.univ fun j => (-1) ^ (↑j + 1) • f (Fin.contractNth j (fun x x_1 => x * x_1) g)) =
    ↑(↑(ρ A) (g 0))
        (f fun i =>
          (Fin.partialProd g (Fin.castSucc (Fin.castSucc i)) * g (Fin.castSucc i))⁻¹ *
            (Fin.partialProd g (Fin.castSucc (Fin.succ i)) * g (Fin.succ i))) +
      Finset.sum Finset.univ fun i =>
        ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
          ((-1) ^ ↑(Fin.succ i) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ i)) 1)
[PROOFSTEP]
rcongr x
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
⊢ g (Fin.succ x) =
    (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)) * g (Fin.castSucc x))⁻¹ *
      (Fin.partialProd g (Fin.castSucc (Fin.succ x)) * g (Fin.succ x))
[PROOFSTEP]
have := Fin.partialProd_right_inv g (Fin.castSucc x)
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
this :
  (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ * Fin.partialProd g (Fin.succ (Fin.castSucc x)) =
    g (Fin.castSucc x)
⊢ g (Fin.succ x) =
    (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)) * g (Fin.castSucc x))⁻¹ *
      (Fin.partialProd g (Fin.castSucc (Fin.succ x)) * g (Fin.succ x))
[PROOFSTEP]
simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢
[GOAL]
case h.h.e_a.h.e_6.h.e_a.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin n
this :
  (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ * Fin.partialProd g (Fin.succ (Fin.castSucc x)) =
    g (Fin.castSucc x)
⊢ g (Fin.succ x) =
    (g (Fin.castSucc x))⁻¹ * (Fin.partialProd g (Fin.castSucc (Fin.castSucc x)))⁻¹ *
      (Fin.partialProd g (Fin.succ (Fin.castSucc x)) * g (Fin.succ x))
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left]
[GOAL]
case h.h.e_a.e_f.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → CoeSort.coe A
g : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (-1) ^ (↑x + 1) • f (Fin.contractNth x (fun x x_1 => x * x_1) g) =
    ↑(↑(LinearEquiv.symm (diagonalHomEquiv n A)) f).hom
      ((-1) ^ ↑(Fin.succ x) • Finsupp.single (Fin.partialProd g ∘ Fin.succAbove (Fin.succ x)) 1)
[PROOFSTEP]
rw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (fun n => d n A) n ≫ (fun n => d n A) (n + 1) = 0
[PROOFSTEP]
ext x
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2))
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1) ≫
            HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        x =
      ↑0 x
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
simp only [ModuleCat.comp_def, LinearMap.comp_apply] at this
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑((fun n => d n A) n ≫ (fun n => d n A) (n + 1)) x = ↑0 x
[PROOFSTEP]
dsimp only
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑(d n A ≫ d (n + 1) A) x = ↑0 x
[PROOFSTEP]
simp only [d_eq, LinearEquiv.toModuleIso_inv, LinearEquiv.toModuleIso_hom, ModuleCat.coe_comp, Function.comp_apply]
  /- Porting note: I can see I need to rewrite `LinearEquiv.coe_coe` twice to at
        least reduce the need for `symm_apply_apply` to be an `erw`. However, even `erw` refuses to
        rewrite the second `coe_coe`... -/
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑↑(Rep.diagonalHomEquiv (n + 1 + 1) A)
      (↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 1 + 1))
        (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv (n + 1) A))
          (↑↑(Rep.diagonalHomEquiv (n + 1) A)
            (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1))
              (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) x))))) =
    ↑0 x
[PROOFSTEP]
erw [LinearEquiv.symm_apply_apply, this]
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
x : ↑((fun n => ModuleCat.of k ((Fin n → G) → CoeSort.coe A)) n)
this :
  ∀ (x : ↑(HomologicalComplex.X (linearYonedaObjResolution A) n)),
    ↑(HomologicalComplex.d (linearYonedaObjResolution A) (n + 1) (n + 2))
        (↑(HomologicalComplex.d (linearYonedaObjResolution A) n (n + 1)) x) =
      ↑0 x
⊢ ↑↑(Rep.diagonalHomEquiv (n + 1 + 1) A) (↑0 (↑↑(LinearEquiv.symm (Rep.diagonalHomEquiv n A)) x)) = ↑0 x
[PROOFSTEP]
exact map_zero _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ inhomogeneousCochains A ≅ linearYonedaObjResolution A
[PROOFSTEP]
refine' HomologicalComplex.Hom.isoOfComponents (fun i => (Rep.diagonalHomEquiv i A).toModuleIso.symm) _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ ∀ (i j : ℕ),
    ComplexShape.Rel (ComplexShape.up ℕ) i j →
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
          HomologicalComplex.d (linearYonedaObjResolution A) i j =
        HomologicalComplex.d (inhomogeneousCochains A) i j ≫
          ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) j).hom
[PROOFSTEP]
rintro i j (h : i + 1 = j)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i j : ℕ
h : i + 1 = j
⊢ ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
      HomologicalComplex.d (linearYonedaObjResolution A) i j =
    HomologicalComplex.d (inhomogeneousCochains A) i j ≫
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) j).hom
[PROOFSTEP]
subst h
[GOAL]
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i : ℕ
⊢ ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) i).hom ≫
      HomologicalComplex.d (linearYonedaObjResolution A) i (i + 1) =
    HomologicalComplex.d (inhomogeneousCochains A) i (i + 1) ≫
      ((fun i => (LinearEquiv.toModuleIso (Rep.diagonalHomEquiv i A)).symm) (i + 1)).hom
[PROOFSTEP]
simp only [CochainComplex.of_d, d_eq, Category.assoc, Iso.symm_hom, Iso.hom_inv_id, Category.comp_id]


[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ toNat a < b ↔ a < ↑b
[PROOFSTEP]
rw [← toNat_lt_toNat, toNat_coe_nat]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < ↑b
[PROOFSTEP]
exact coe_nat_pos.2 hb.bot_lt
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = ↑0 * ↑n
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m k : ℤ
x✝ : 0 ≤ k
ih : ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n
n : ℤ
⊢ ↑((k + 1) * n) = ↑(k + 1) * ↑n
[PROOFSTEP]
simp [add_mul, ih]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
m k : ℤ
x✝ : k ≤ 0
ih : ∀ (n : ℤ), ↑(k * n) = ↑k * ↑n
n : ℤ
⊢ ↑((k - 1) * n) = ↑(k - 1) * ↑n
[PROOFSTEP]
simp [sub_mul, ih]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x
[PROOFSTEP]
simpa using n.cast_commute x
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x
[PROOFSTEP]
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using (n + 1).cast_commute (-x)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
⊢ Monotone fun x => ↑x
[PROOFSTEP]
intro m n h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
[PROOFSTEP]
rw [← sub_nonneg] at h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h✝ : m ≤ n
h : 0 ≤ n - m
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
[PROOFSTEP]
lift n - m to ℕ using h with k hk
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n
[PROOFSTEP]
rw [← sub_nonneg, ← cast_sub, ← hk, cast_ofNat]
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
[PROOFSTEP]
exact k.cast_nonneg
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑↑n ↔ 0 ≤ ↑n
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
[PROOFSTEP]
have : -(n : α) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ -↑n ≤ 0
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
[PROOFSTEP]
simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
m n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ n
[PROOFSTEP]
rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ ↑n ≤ 0 ↔ n ≤ 0
[PROOFSTEP]
rw [← cast_zero, cast_le]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ 0 < ↑n ↔ 0 < n
[PROOFSTEP]
rw [← cast_zero, cast_lt]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℤ
⊢ ↑n < 0 ↔ n < 0
[PROOFSTEP]
rw [← cast_zero, cast_lt]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
⊢ ↑|a| = |↑a|
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : 0 < a
⊢ 1 ≤ ↑a
[PROOFSTEP]
exact_mod_cast Int.add_one_le_of_lt h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ ↑a ≤ -1
[PROOFSTEP]
rw [← Int.cast_one, ← Int.cast_neg, cast_le]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
h : a < 0
⊢ a ≤ -1
[PROOFSTEP]
exact Int.le_sub_one_of_lt h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
have hnx : 0 < n → 0 ≤ x + n := fun hn =>
  by
  have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
  rwa [add_left_neg] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n
[PROOFSTEP]
have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n
[PROOFSTEP]
rwa [add_left_neg] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
have hnx' : n < 0 → x + n ≤ 0 := fun hn =>
  by
  have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
  rwa [add_right_neg] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0
[PROOFSTEP]
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0
[PROOFSTEP]
rwa [add_right_neg] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n
[PROOFSTEP]
rw [← mul_add, mul_nonneg_iff]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
rcases lt_trichotomy n 0 with (h | rfl | h)
[GOAL]
case inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
exact Or.inr ⟨by exact_mod_cast h.le, hnx' h⟩
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ ↑n ≤ 0
[PROOFSTEP]
exact_mod_cast h.le
[GOAL]
case inr.inl
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
[PROOFSTEP]
simp [le_total 0 x]
[GOAL]
case inr.inr
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
[PROOFSTEP]
exact Or.inl ⟨by exact_mod_cast h.le, hnx h⟩
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact_mod_cast h.le
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b n : ℤ
⊢ ↑(natAbs n) = ↑|n|
[PROOFSTEP]
cases n
[GOAL]
case ofNat
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs (ofNat a✝)) = ↑|ofNat a✝|
[PROOFSTEP]
simp
[GOAL]
case negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : LinearOrderedRing α
a b : ℤ
a✝ : ℕ
⊢ ↑(natAbs -[a✝+1]) = ↑|-[a✝+1]|
[PROOFSTEP]
rw [abs_eq_natAbs, natAbs_negSucc, cast_succ, cast_ofNat, cast_succ]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : ↑f 1 = 1
⊢ ↑f 1 = ↑(castAddHom A) 1
[PROOFSTEP]
simp [h1]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
⊢ f = g
[PROOFSTEP]
ext (x | x)
[GOAL]
case h.ofNat
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (ofNat x) = ↑g (ofNat x)
[PROOFSTEP]
exact (FunLike.congr_fun h_nat x : _)
[GOAL]
case h.negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f -[x+1] = ↑g -[x+1]
[PROOFSTEP]
rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
[GOAL]
case h.negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (-1) * ↑f (↑x + 1) = ↑g (-1) * ↑g (↑x + 1)
[PROOFSTEP]
congr 1
[GOAL]
case h.negSucc.e_a
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : ↑f (-1) = ↑g (-1)
h_nat : comp f ↑ofNatHom = comp g ↑ofNatHom
x : ℕ
⊢ ↑f (↑x + 1) = ↑g (↑x + 1)
[PROOFSTEP]
exact_mod_cast (FunLike.congr_fun h_nat (x + 1) : _)


[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ (a : α), a ∈ s → f a ∈ t
hb : card t • b < ∑ x in s, w x
⊢ ∑ i in t, b < ∑ i in t, ∑ x in filter (fun x => f x = i) s, w x
[PROOFSTEP]
simpa only [sum_fiberwise_of_maps_to hf, sum_const]
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
ht : ∀ (y : β), ¬y ∈ t → ∑ x in filter (fun x => f x = y) s, w x ≤ 0
hb : card t • b < ∑ x in s, w x
⊢ ∑ _y in t, b < ∑ x in s, w x
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ x in s, w x
⊢ ∑ i in t, b ≤ ∑ i in t, ∑ x in filter (fun x => f x = i) s, w x
[PROOFSTEP]
simpa only [sum_fiberwise_of_maps_to hf, sum_const]
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ (y : β), ¬y ∈ t → ∑ x in filter (fun x => f x = y) s, w x ≤ 0
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ x in s, w x
⊢ ∑ _y in t, b ≤ ∑ x in s, w x
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : card t • b < ↑(card s)
⊢ ∃ y, y ∈ t ∧ b < ↑(card (filter (fun x => f x = y) s))
[PROOFSTEP]
simp_rw [cast_card] at ht ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : card t • b < ∑ a in s, 1
⊢ ∃ y, y ∈ t ∧ b < ∑ a in filter (fun x => f x = y) s, 1
[PROOFSTEP]
exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : ↑(card s) < card t • b
⊢ ∃ y, y ∈ t ∧ ↑(card (filter (fun x => f x = y) s)) < b
[PROOFSTEP]
simp_rw [cast_card] at ht ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : ∑ a in s, 1 < card t • b
⊢ ∃ y, y ∈ t ∧ ∑ a in filter (fun x => f x = y) s, 1 < b
[PROOFSTEP]
exact exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ↑(card s)
⊢ ∃ y, y ∈ t ∧ b ≤ ↑(card (filter (fun x => f x = y) s))
[PROOFSTEP]
simp_rw [cast_card] at hb ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ a in s, 1
⊢ ∃ y, y ∈ t ∧ b ≤ ∑ a in filter (fun x => f x = y) s, 1
[PROOFSTEP]
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : Finset.Nonempty t
hb : ↑(card s) ≤ card t • b
⊢ ∃ y, y ∈ t ∧ ↑(card (filter (fun x => f x = y) s)) ≤ b
[PROOFSTEP]
simp_rw [cast_card] at hb ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : Finset.Nonempty t
hb : ∑ a in s, 1 ≤ card t • b
⊢ ∃ y, y ∈ t ∧ ∑ a in filter (fun x => f x = y) s, 1 ≤ b
[PROOFSTEP]
refine' exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb


[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n
[PROOFSTEP]
rw [← cast_add, Nat.sub_add_cancel h]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1
[PROOFSTEP]
cases h
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1
[PROOFSTEP]
rw [cast_succ, add_sub_cancel]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : AddGroupWithOne R
n : ℕ
inst✝ : AtLeastTwo n
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n
[PROOFSTEP]
simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
erw [cast_ofNat, Nat.cast_one]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0
[PROOFSTEP]
erw [cast_zero, neg_zero]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)
[PROOFSTEP]
erw [cast_ofNat, cast_negSucc]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(- -[n+1]) = -↑-[n+1]
[PROOFSTEP]
erw [cast_ofNat, cast_negSucc, neg_neg]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n
[PROOFSTEP]
unfold subNatNat
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
cases e : n - m
[GOAL]
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑(match zero with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
simp only [ofNat_eq_coe]
[GOAL]
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑↑(m - n) = ↑m - ↑n
[PROOFSTEP]
simp [e, Nat.le_of_sub_eq_zero e]
[GOAL]
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = succ n✝
⊢ ↑(match succ n✝ with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
rw [cast_negSucc, Nat.add_one, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(negOfNat n) = -↑n
[PROOFSTEP]
simp [Int.cast_neg, negOfNat_eq]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n
[PROOFSTEP]
simp [← Int.ofNat_add, Nat.cast_add]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]
[PROOFSTEP]
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n
[PROOFSTEP]
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ←
  Nat.cast_add, Nat.add_comm]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[m + n + 1+1] = ↑-[m+1] + ↑-[n+1]
[PROOFSTEP]
rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc,
  Nat.add_comm]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℤ
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ ↑(bit1 n) = bit1 ↑n
[PROOFSTEP]
rw [bit1, Int.cast_add, Int.cast_one, cast_bit0]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ bit0 ↑n + 1 = bit1 ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑2 = ↑2
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑3 = ↑3
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑4 = ↑4
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ ↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm f
[PROOFSTEP]
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
[PROOFSTEP]
induction' p with y z p a ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p
⊢ listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)
[PROOFSTEP]
dsimp at *
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = p
⊢ Path.cons (listToPath (pathToList p)) a = Path.cons p a
[PROOFSTEP]
rw [ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
⊢ pathToList (listToPath l) = l
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ pathToList (listToPath []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l
[PROOFSTEP]
change a :: pathToList (listToPath l) = a :: l
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
[PROOFSTEP]
rw [ih]


[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')
[PROOFSTEP]
{rw [hu, hv]
}
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')
[PROOFSTEP]
rw [hu, hv]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e = _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ cast (_ : u' = u') (_ : v' = v') e = _root_.cast (_ : (u' ⟶ v') = (u' ⟶ v')) e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast (_ : u = u'') (_ : v = v'') e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
e : u'' ⟶ v''
⊢ cast (_ : u'' = u'') (_ : v'' = v'') (cast (_ : u'' = u'') (_ : v'' = v'') e) = cast (_ : u'' = u'') (_ : v'' = v'') e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ HEq (cast hu hv e) e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast (_ : u' = u') (_ : v' = v') e) e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ HEq e e'
[PROOFSTEP]
rw [Hom.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e = e' ↔ HEq e e'
[PROOFSTEP]
exact _root_.cast_eq_iff_heq
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ HEq e' e
[PROOFSTEP]
rw [eq_comm, Hom.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ HEq e e' ↔ HEq e' e
[PROOFSTEP]
exact ⟨HEq.symm, HEq.symm⟩
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'
[PROOFSTEP]
rw [hu, hv]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p = _root_.cast (_ : Path u v = Path u' v') p
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
p : Path u' v'
⊢ cast (_ : u' = u') (_ : v' = v') p = _root_.cast (_ : Path u' v' = Path u' v') p
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
p : Path u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv p) = cast (_ : u = u'') (_ : v = v'') p
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
p : Path u'' v''
⊢ cast (_ : u'' = u'') (_ : v'' = v'') (cast (_ : u'' = u'') (_ : v'' = v'') p) = cast (_ : u'' = u'') (_ : v'' = v'') p
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast (_ : u' = u') (_ : u' = u') nil = nil
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (cast hu hv p) p
[PROOFSTEP]
rw [Path.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (_root_.cast (_ : Path u v = Path u' v') p) p
[PROOFSTEP]
exact _root_.cast_heq _ _
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ cast hu hv p = p' ↔ HEq p p'
[PROOFSTEP]
rw [Path.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ _root_.cast (_ : Path u v = Path u' v') p = p' ↔ HEq p p'
[PROOFSTEP]
exact _root_.cast_eq_iff_heq
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v w u' w' : U
p : Path u v
e : v ⟶ w
hu : u = u'
hw : w = w'
⊢ cast hu hw (cons p e) = cons (cast hu (_ : v = v) p) (Hom.cast (_ : v = v) hw e)
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
v u' w' : U
p : Path u' v
e : v ⟶ w'
⊢ cast (_ : u' = u') (_ : w' = w') (cons p e) =
    cons (cast (_ : u' = u') (_ : v = v) p) (Hom.cast (_ : v = v) (_ : w' = w') e)
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Path.cast (_ : u = u) (_ : v = v') p = p'
[PROOFSTEP]
rw [Path.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq p p'
[PROOFSTEP]
exact heq_of_cons_eq_cons h
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Hom.cast (_ : v = v') (_ : w = w) e = e'
[PROOFSTEP]
rw [Hom.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq e e'
[PROOFSTEP]
exact hom_heq_of_cons_eq_cons h
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : length p = 0
⊢ Path.cast (_ : u = v) (_ : v = v) p = nil
[PROOFSTEP]
cases p
[GOAL]
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : length nil = 0
⊢ Path.cast (_ : u = u) (_ : u = u) nil = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : length (cons a✝¹ a✝) = 0
⊢ Path.cast (_ : u = v) (_ : v = v) (cons a✝¹ a✝) = nil
[PROOFSTEP]
simp only [Nat.succ_ne_zero, length_cons] at hzero


[GOAL]
M : Type ?u.870
inst✝ : Semigroup M
src✝ : Mul (Ultrafilter M) := mul
U V W : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (x : M) in ↑(U * V * W), p x) ↔ ∀ᶠ (x : M) in ↑(U * (V * W)), p x
[PROOFSTEP]
simp_rw [Ultrafilter.eventually_mul, mul_assoc]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
[PROOFSTEP]
induction' hm with a a m hm ih a m hm ih
[GOAL]
case head
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m : M
a : Stream' M
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m' ∈ FP a
[PROOFSTEP]
exact ⟨1, fun m hm => FP.cons a m hm⟩
[GOAL]
case tail
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
ih : ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
[PROOFSTEP]
cases' ih with n hn
[GOAL]
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
[PROOFSTEP]
use n + 1
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → m * m' ∈ FP a
[PROOFSTEP]
intro m' hm'
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a
[PROOFSTEP]
exact FP.tail _ _ (hn _ hm')
[GOAL]
case cons
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
ih : ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
[PROOFSTEP]
cases' ih with n hn
[GOAL]
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
[PROOFSTEP]
use n + 1
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → Stream'.head a * m * m' ∈ FP a
[PROOFSTEP]
intro m' hm'
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * m * m' ∈ FP a
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * (m * m') ∈ FP a
[PROOFSTEP]
exact FP.cons _ _ (hn _ hm')
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
let S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ m in U, m ∈ FP (a.drop n)}
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
[GOAL]
case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
h : ∃ m, m ∈ S ∧ m * m = m
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
rcases h with ⟨U, hU, U_idem⟩
[GOAL]
case refine_5.intro.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
refine' ⟨U, U_idem, _⟩
[GOAL]
case refine_5.intro.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
convert Set.mem_iInter.mp hU 0
[GOAL]
case refine_1
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (r : Ultrafilter M), Continuous fun x => x * r
[PROOFSTEP]
exact Ultrafilter.continuous_mul_left
[GOAL]
case refine_2
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ Set.Nonempty S
[PROOFSTEP]
apply IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (i + 1) a)} ⊆ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n U hU
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
apply Eventually.mono hU
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ (x : M), x ∈ FP (Stream'.drop (n + 1) a) → x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
rw [add_comm, ← Stream'.drop_drop, ← Stream'.tail_eq_drop]
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ (x : M), x ∈ FP (Stream'.tail (Stream'.drop n a)) → x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
exact FP.tail _
[GOAL]
case refine_2.hZn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), Set.Nonempty {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_2.hZn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ Set.Nonempty {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
[GOAL]
case refine_2.hZ0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}
[PROOFSTEP]
exact (ultrafilter_isClosed_basic _).isCompact
[GOAL]
case refine_2.hZcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_2.hZcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
apply ultrafilter_isClosed_basic
[GOAL]
case refine_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S
[PROOFSTEP]
exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (x : Ultrafilter M), x ∈ S → ∀ (y : Ultrafilter M), y ∈ S → x * y ∈ S
[PROOFSTEP]
intro U hU V hV
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
V : Ultrafilter M
hV : V ∈ S
⊢ U * V ∈ S
[PROOFSTEP]
rw [Set.mem_iInter] at *
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
⊢ ∀ (i : ℕ), U * V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ U * V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply Eventually.mono (hU n)
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ (x : M), x ∈ FP (Stream'.drop n a) → ∀ᶠ (m' : M) in ↑V, x * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
intro m hm
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
obtain ⟨n', hn⟩ := FP.mul hm
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply Eventually.mono (hV (n' + n))
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ (x : M), x ∈ FP (Stream'.drop (n' + n) a) → m * x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
intro m' hm'
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply hn
[GOAL]
case refine_4.intro.a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m' ∈ FP (Stream'.drop n' (Stream'.drop n a))
[PROOFSTEP]
simpa only [Stream'.drop_drop] using hm'
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
have exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m | ∀ᶠ m' in U, m * m' ∈ s}).Nonempty := fun {s} hs =>
  Ultrafilter.nonempty_of_mem (inter_mem hs <| by rwa [← U_idem] at hs )
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
s : Set M
hs : s ∈ U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U
[PROOFSTEP]
rwa [← U_idem] at hs
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
let succ : { s // s ∈ U } → { s // s ∈ U } := fun (p : { s // s ∈ U }) =>
  ⟨p.val ∩ {m : M | elem p * m ∈ p.val},
    inter_mem p.property
      (show (exists_elem p.property).some ∈ {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} from
        p.val.inter_subset_right {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} (exists_elem p.property).some_mem)⟩
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
use Stream'.corec elem succ (Subtype.mk s₀ sU)
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ FP (Stream'.corec elem succ { val := s₀, property := sU }) ⊆ s₀
[PROOFSTEP]
suffices ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ p, a = Stream'.corec elem succ p → m ∈ p.val
  by
  intro m hm
  exact this _ m hm ⟨s₀, sU⟩ rfl
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
this : ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
⊢ FP (Stream'.corec elem succ { val := s₀, property := sU }) ⊆ s₀
[PROOFSTEP]
intro m hm
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
this : ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
m : M
hm : m ∈ FP (Stream'.corec elem succ { val := s₀, property := sU })
⊢ m ∈ s₀
[PROOFSTEP]
exact this _ m hm ⟨s₀, sU⟩ rfl
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
clear sU s₀
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
intro a m h
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
h : m ∈ FP a
⊢ ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
induction' h with b b n h ih b n h ih
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → Stream'.head b ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ Stream'.head (Stream'.corec elem succ p) ∈ ↑p
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.head_cons]
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ elem p ∈ ↑p
[PROOFSTEP]
exact Set.inter_subset_left _ _ (Set.Nonempty.some_mem _)
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
n : M
h : FP (Stream'.tail b) n
ih : ∀ (p : { s // s ∈ U }), Stream'.tail b = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ n ∈ ↑p
[PROOFSTEP]
refine' Set.inter_subset_left _ _ (ih (succ p) _)
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ (succ p)
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.tail_cons]
[GOAL]
case h.cons
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
n : M
h : FP (Stream'.tail b) n
ih : ∀ (p : { s // s ∈ U }), Stream'.tail b = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → Stream'.head b * n ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.cons
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.head (Stream'.corec elem succ p) * n ∈ ↑p
[PROOFSTEP]
have := Set.inter_subset_right _ _ (ih (succ p) ?_)
[GOAL]
case h.cons.refine_2
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
this : n ∈ {m | elem p * m ∈ ↑p}
⊢ Stream'.head (Stream'.corec elem succ p) * n ∈ ↑p
[PROOFSTEP]
simpa only using this
[GOAL]
case h.cons.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ (succ p)
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.tail_cons]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop Nat.zero a) ⊆ FP a
[PROOFSTEP]
rfl
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (Nat.succ n) a) ⊆ FP a
[PROOFSTEP]
rw [Nat.succ_eq_one_add, ← Stream'.drop_drop]
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
[PROOFSTEP]
exact _root_.trans (FP.tail _) ih
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ Stream'.nth a i ∈ FP a
[PROOFSTEP]
induction' i with i ih generalizing a
[GOAL]
case zero
M : Type u_1
inst✝ : Semigroup M
a✝ a : Stream' M
⊢ Stream'.nth a Nat.zero ∈ FP a
[PROOFSTEP]
apply FP.head
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ Stream'.nth a (Nat.succ i) ∈ FP a
[PROOFSTEP]
apply FP.tail
[GOAL]
case succ.h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ FP (Stream'.tail a) (Stream'.nth a (Nat.succ i))
[PROOFSTEP]
apply ih
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.nth a i * Stream'.nth a j ∈ FP a
[PROOFSTEP]
refine' FP_drop_subset_FP _ i _
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.nth a i * Stream'.nth a j ∈ FP (Stream'.drop i a)
[PROOFSTEP]
rw [← Stream'.head_drop]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.head (Stream'.drop i a) * Stream'.nth a j ∈ FP (Stream'.drop i a)
[PROOFSTEP]
apply FP.cons
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
[PROOFSTEP]
rcases le_iff_exists_add.mp (Nat.succ_le_of_lt ij) with
  ⟨d, hd⟩
    -- Porting note: need to fix breakage of Set notation
[GOAL]
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
[PROOFSTEP]
change _ ∈ FP _
[GOAL]
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
[PROOFSTEP]
have := FP.singleton (a.drop i).tail d
[GOAL]
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth (Stream'.tail (Stream'.drop i a)) d ∈ FP (Stream'.tail (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
[PROOFSTEP]
rw [Stream'.tail_eq_drop, Stream'.nth_drop, Stream'.nth_drop] at this
[GOAL]
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4.h.e'_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ j = d + 1 + i
[PROOFSTEP]
rw [hd, add_comm, Nat.succ_add, Nat.add_succ]
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP a
[PROOFSTEP]
refine' FP_drop_subset_FP _ (s.min' hs) _
[GOAL]
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
induction' s using Finset.strongInduction with s ih
[GOAL]
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]
[GOAL]
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
cases' (s.erase (s.min' hs)).eq_empty_or_nonempty with h h
[GOAL]
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
rw [h, Finset.prod_empty, mul_one]
[GOAL]
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ Stream'.head (Stream'.drop (Finset.min' s hs) a) ∈ FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
exact FP.head _
[GOAL]
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
[PROOFSTEP]
apply FP.cons
[GOAL]
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.tail (Stream'.drop (Finset.min' s hs) a))
    (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
[PROOFSTEP]
rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
[GOAL]
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' s hs + 1) a) (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
[PROOFSTEP]
refine' Set.mem_of_subset_of_mem _ (ih _ (Finset.erase_ssubset <| s.min'_mem hs) h)
[GOAL]
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
[PROOFSTEP]
have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
  Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)
[GOAL]
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
[PROOFSTEP]
cases' le_iff_exists_add.mp this with d hd
[GOAL]
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
[PROOFSTEP]
rw [hd, add_comm, ← Stream'.drop_drop]
[GOAL]
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (Finset.min' s hs + 1) a)) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
[PROOFSTEP]
apply FP_drop_subset_FP


[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (fun X Y x => τ X ⟶ τ Y) (σ X) (σ Y) (PushQuiver.arrow f)
[PROOFSTEP]
dsimp only
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)
[PROOFSTEP]
rw [← h X, ← h Y]
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.obj X ⟶ φ.obj Y
[PROOFSTEP]
exact φ.map f
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ of σ ⋙q lift σ φ τ h = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
[PROOFSTEP]
simp only [Prefunctor.comp_obj]
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.obj X
[PROOFSTEP]
apply Eq.symm
[GOAL]
case h_obj.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)
[PROOFSTEP]
exact h X
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of σ ⋙q lift σ φ τ h).map f =
      Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
        (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
      (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
[PROOFSTEP]
simp only [Prefunctor.comp_map]
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) =
    (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
iterate 2 apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply HEq.symm
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
apply (eqRec_heq _ _).trans
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
have : ∀ {α γ} {β : α → γ → Sort _} {a a'} (p : a = a') g (b : β a g), HEq (p ▸ b) b :=
  by
  intros
  subst_vars
  rfl
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ ∀ {α : Sort ?u.2529} {γ : Sort ?u.2531} {β : α → γ → Sort ?u.2533} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
[PROOFSTEP]
intros
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2529
γ✝ : Sort ?u.2531
β✝ : α✝ → γ✝ → Sort ?u.2533
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝
[PROOFSTEP]
subst_vars
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2529
γ✝ : Sort ?u.2531
β✝ : α✝ → γ✝ → Sort ?u.2533
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq ((_ : a'✝ = a'✝) ▸ b✝) b✝
[PROOFSTEP]
rfl
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2529} {γ : Sort ?u.2531} {β : α → γ → Sort ?u.2533} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
apply this
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ = lift σ φ τ h
[PROOFSTEP]
dsimp only [of, lift]
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ =
    { obj := τ,
      map :=
        @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
          id
            (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
              (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ,
            map :=
              @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                id
                  (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                    (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
        X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ,
          map :=
            @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
              id
                (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                  (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
      X
[PROOFSTEP]
simp only
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X
[PROOFSTEP]
rw [Φ₀]
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn
        (_ :
          { obj := τ,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                          (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
              Y =
            Φ.obj Y)
        (Eq.recOn
          (_ :
            { obj := τ,
                    map :=
                      @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                        id
                          (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                            (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
                X =
              Φ.obj X)
          ({ obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                        (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.map
            f))
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn
      (_ :
        { obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                        (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
            (σ Y✝) =
          Φ.obj (σ Y✝))
      (Eq.recOn
        (_ :
          { obj := τ,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                          (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
              (σ X✝) =
            Φ.obj (σ X✝))
        ({ obj := τ,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                  id
                    (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                      (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.map
          (PushQuiver.arrow f✝)))
[PROOFSTEP]
subst_vars
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn
      (_ :
        { obj := Φ.obj,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                        (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                          ((of σ ⋙q Φ).map f))) }.obj
            (σ Y✝) =
          Φ.obj (σ Y✝))
      (Eq.recOn
        (_ :
          { obj := Φ.obj,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                          (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                            ((of σ ⋙q Φ).map f))) }.obj
              (σ X✝) =
            Φ.obj (σ X✝))
        ({ obj := Φ.obj,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                  id
                    (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                      (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                        ((of σ ⋙q Φ).map f))) }.map
          (PushQuiver.arrow f✝)))
[PROOFSTEP]
simp only [Prefunctor.comp_map, cast_eq]
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    id
      (Eq.mpr (_ : (Φ.obj (σ X✝) ⟶ Φ.obj (σ Y✝)) = ((of σ ⋙q Φ).obj X✝ ⟶ Φ.obj (σ Y✝)))
        (Eq.mpr (_ : ((of σ ⋙q Φ).obj X✝ ⟶ Φ.obj (σ Y✝)) = ((of σ ⋙q Φ).obj X✝ ⟶ (of σ ⋙q Φ).obj Y✝))
          (Φ.map ((of σ).map f✝))))
[PROOFSTEP]
rfl