[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) ↔ ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
intro hS
[GOAL]
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S
[PROOFSTEP]
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
[GOAL]
case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)
[PROOFSTEP]
rintro ⟨T, rfl⟩
[GOAL]
case mpr.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))
[PROOFSTEP]
exact Hld T
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ ⊤ ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
[PROOFSTEP]
change K _ _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G ⊤)
[PROOFSTEP]
rw [Sieve.functorPushforward_top]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
⊢ GrothendieckTopology.sieves K (G.obj X) ⊤
[PROOFSTEP]
exact K.top_mem _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
have : S.pullback f = ((S.functorPushforward G).pullback (G.map f)).functorPullback G :=
  by
  conv_lhs => rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
  ext
  change (S.functorPushforward G) _ ↔ (S.functorPushforward G) _
  rw [G.map_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
[PROOFSTEP]
conv_lhs => rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
| Sieve.pullback f S
[PROOFSTEP]
rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
⊢ Sieve.pullback f (Sieve.functorPullback G (Sieve.functorPushforward G S)) =
    Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (Sieve.pullback f (Sieve.functorPullback G (Sieve.functorPushforward G S))).arrows f✝ ↔
    (Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))).arrows f✝
[PROOFSTEP]
change (S.functorPushforward G) _ ↔ (S.functorPushforward G) _
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
Y✝ : C
f✝ : Y✝ ⟶ Y
⊢ (Sieve.functorPushforward G S).arrows (G.map (f✝ ≫ f)) ↔ (Sieve.functorPushforward G S).arrows (G.map f✝ ≫ G.map f)
[PROOFSTEP]
rw [G.map_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ Sieve.pullback f S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S)) ∈
    (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
[PROOFSTEP]
change K _ _
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
this : Sieve.pullback f S = Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))
⊢ GrothendieckTopology.sieves K (G.obj Y)
    (Sieve.functorPushforward G (Sieve.functorPullback G (Sieve.pullback (G.map f) (Sieve.functorPushforward G S))))
[PROOFSTEP]
apply Hld ⟨_, K.pullback_stable (G.map f) hS⟩
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
⊢ S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
[PROOFSTEP]
apply K.transitive hS
[GOAL]
case h
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄,
    (Sieve.functorPushforward G S).arrows f →
      Sieve.pullback f (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
rintro Y _ ⟨Z, g, i, hg, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
rw [Sieve.pullback_comp]
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ GrothendieckTopology.sieves K Y
[PROOFSTEP]
apply K.pullback_stable i
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (G.map g) (Sieve.functorPushforward G S') ∈ GrothendieckTopology.sieves K (G.obj Z)
[PROOFSTEP]
refine' K.superset_covering _ (H' hg)
[GOAL]
case h.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.functorPushforward G (Sieve.pullback g S') ≤ Sieve.pullback (G.map g) (Sieve.functorPushforward G S')
[PROOFSTEP]
rintro W _ ⟨Z', g', i', hg, rfl⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg✝ : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')).arrows (i' ≫ G.map g')
[PROOFSTEP]
refine' ⟨Z', g' ≫ g, i', hg, _⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁴ : Category.{?u.3052, u_1} C
D : Type u_2
inst✝³ : Category.{?u.3059, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝² : Category.{u, v} A
inst✝¹ : Full G
inst✝ : Faithful G
Hld : LocallyCoverDense K G
X : C
S : Sieve X
hS : S ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) X
S' : Sieve X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Sieve.pullback f S' ∈ (fun X S => GrothendieckTopology.sieves K (G.obj X) (Sieve.functorPushforward G S)) Y
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg✝ : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (i' ≫ G.map g') ≫ G.map g = i' ≫ G.map (g' ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
⊢ LocallyCoverDense K G
[PROOFSTEP]
intro X T
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ GrothendieckTopology.sieves K (G.obj X)
[PROOFSTEP]
refine' K.superset_covering _ (K.bind_covering T.property fun Y f _ => H.is_cover Y)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
⊢ (Sieve.bind (↑T).arrows fun Y f x => Sieve.coverByImage G Y) ≤ Sieve.functorPushforward G (Sieve.functorPullback G ↑T)
[PROOFSTEP]
rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', rfl : _ = _⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.mk
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)).arrows ((g ≫ f') ≫ f)
[PROOFSTEP]
use W
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ g_1 h, (Sieve.functorPullback G ↑T).arrows g_1 ∧ (g ≫ f') ≫ f = h ≫ G.map g_1
[PROOFSTEP]
use G.preimage (f' ≫ f)
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ ∃ h, (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = h ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
use g
[GOAL]
case h
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f)) ∧ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
constructor
[GOAL]
case h.left
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (Sieve.functorPullback G ↑T).arrows (G.preimage (f' ≫ f))
case h.right
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
simpa using T.val.downward_closed hf f'
[GOAL]
case h.right
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝¹ : Category.{u, v} A
inst✝ : Full G
H : CoverDense K G
X : C
T : ↑(GrothendieckTopology.sieves K (G.obj X))
Y Z : D
f : Z ⟶ G.obj X
hf : (↑T).arrows f
W : C
g : Y ⟶ G.obj W
f' : G.obj W ⟶ Z
⊢ (g ≫ f') ≫ f = g ≫ G.map (G.preimage (f' ≫ f))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
⊢ LocallyCoverDense J (Over.forget X)
[PROOFSTEP]
intro Y T
[GOAL]
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) ∈
    GrothendieckTopology.sieves J ((Over.forget X).obj Y)
[PROOFSTEP]
convert T.property
[GOAL]
case h.e'_4
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) = ↑T
[PROOFSTEP]
ext Z f
[GOAL]
case h.e'_4.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
[PROOFSTEP]
constructor
[GOAL]
case h.e'_4.h.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f → (↑T).arrows f
[PROOFSTEP]
rintro ⟨_, _, g', hg, rfl⟩
[GOAL]
case h.e'_4.h.mp.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
w✝¹ : Over X
w✝ : w✝¹ ⟶ Y
g' : Z ⟶ (Over.forget X).obj w✝¹
hg : (Sieve.functorPullback (Over.forget X) ↑T).arrows w✝
⊢ (↑T).arrows (g' ≫ (Over.forget X).map w✝)
[PROOFSTEP]
exact T.val.downward_closed hg g'
[GOAL]
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (↑T).arrows f → (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
[PROOFSTEP]
intro hf
[GOAL]
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.13139, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category.{u, v} A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
hf : (↑T).arrows f
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
[PROOFSTEP]
exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩


[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
⊢ f✝ ⊗ 0 = 0
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
⊢ F.map (f✝ ⊗ 0) = F.map 0
[PROOFSTEP]
simp [F.map_tensor]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : Y✝ ⟶ Z✝
⊢ 0 ⊗ f✝ = 0
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : Y✝ ⟶ Z✝
⊢ F.map (0 ⊗ f✝) = F.map 0
[PROOFSTEP]
simp [F.map_tensor]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ (g✝ + h✝) = f✝ ⊗ g✝ + f✝ ⊗ h✝
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ F.map (f✝ ⊗ (g✝ + h✝)) = F.map (f✝ ⊗ g✝ + f✝ ⊗ h✝)
[PROOFSTEP]
simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp, MonoidalPreadditive.tensor_add]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ⊗ h✝ = f✝ ⊗ h✝ + g✝ ⊗ h✝
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ⊗ h✝) = F.map (f✝ ⊗ h✝ + g✝ ⊗ h✝)
[PROOFSTEP]
simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp, MonoidalPreadditive.add_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ f ⊗ ∑ j in s, g j = ∑ j in s, f ⊗ g j
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
let tQ := (((tensoringLeft C).obj Q).mapAddHom : (R ⟶ S) →+ _)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
change _ ≫ tQ _ = _
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ ↑tQ (∑ j in s, g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
rw [tQ.map_sum, Preadditive.comp_sum]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ ↑tQ (g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
dsimp [Functor.mapAddHom]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
simp only [tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (∑ j in s, g j) ⊗ f = ∑ j in s, g j ⊗ f
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
let tQ := (((tensoringRight C).obj P).mapAddHom : (R ⟶ S) →+ _)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
change tQ _ ≫ _ = _
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ↑tQ (∑ j in s, g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
rw [tQ.map_sum, Preadditive.sum_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, ↑tQ (g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
dsimp [Functor.mapAddHom]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, (g j ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
simp only [tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.453496, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, Bicone.π (Functor.mapBicone (tensorLeft X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorLeft X) b) j =
    𝟙 (Functor.mapBicone (tensorLeft X) b).pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.453496, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, (𝟙 X ⊗ Bicone.π b j) ≫ (𝟙 X ⊗ Bicone.ι b j) = 𝟙 (X ⊗ b.pt)
[PROOFSTEP]
simp only [← tensor_comp, Category.comp_id, ← tensor_sum, ← tensor_id, IsBilimit.total i]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.457304, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, Bicone.π (Functor.mapBicone (tensorRight X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorRight X) b) j =
    𝟙 (Functor.mapBicone (tensorRight X) b).pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.457304, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, (Bicone.π b j ⊗ 𝟙 X) ≫ (Bicone.ι b j ⊗ 𝟙 X) = 𝟙 (b.pt ⊗ X)
[PROOFSTEP]
simp only [← tensor_comp, Category.comp_id, ← sum_tensor, ← tensor_id, IsBilimit.total i]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).hom = ∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.lift fun j => 𝟙 X ⊗ biproduct.π f j) ≫ biproduct.π (fun j => X ⊗ f j) j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
erw [biproduct.lift_π]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ 𝟙 X ⊗ biproduct.π f j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero, Finset.sum_dite_eq',
  Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j => X ⊗ f j) j✝ ≫ biproduct.desc fun j => 𝟙 X ⊗ biproduct.ι f j) =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ,
  ite_true, eqToHom_refl, Category.id_comp, biproduct.ι_desc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j = 𝟙 X ⊗ biproduct.π f j
[PROOFSTEP]
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (𝟙 X ⊗ biproduct.ι f j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j
[PROOFSTEP]
simp [leftDistributor_hom, Preadditive.comp_sum, ← id_tensor_comp_assoc, biproduct.ι_π, tensor_dite, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ (𝟙 X ⊗ biproduct.π f j) = biproduct.π (fun j => X ⊗ f j) j
[PROOFSTEP]
simp [leftDistributor_inv, Preadditive.sum_comp, ← id_tensor_comp, biproduct.ι_π, tensor_dite, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j => X ⊗ f j) j ≫ (leftDistributor X f).inv = 𝟙 X ⊗ biproduct.ι f j
[PROOFSTEP]
simp [leftDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
⊢ ((asIso (𝟙 X) ⊗ leftDistributor Y f) ≪≫ leftDistributor X fun j => Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => α_ X Y (f j)
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ ((asIso (𝟙 X) ⊗ leftDistributor Y f) ≪≫ leftDistributor X fun j => Y ⊗ f j).hom ≫
      biproduct.π (fun j => X ⊗ Y ⊗ f j) j✝ =
    ((α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => α_ X Y (f j)).hom ≫
      biproduct.π (fun j => X ⊗ Y ⊗ f j) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum, id_tensor_comp, tensorIso_hom, leftDistributor_hom,
  biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq',
  Finset.sum_const_zero]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫
          (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ (𝟙 X ⊗ biproduct.π (fun j => Y ⊗ f j) j✝)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [← id_tensor_comp, biproduct.ι_π]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J, 𝟙 X ⊗ (𝟙 Y ⊗ biproduct.π f x) ≫ if h : x = j✝ then eqToHom (_ : Y ⊗ f x = Y ⊗ f j✝) else 0
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [id_tensor_comp, tensor_dite, comp_dite]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        if h : x = j✝ then (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ eqToHom (_ : Y ⊗ f x = Y ⊗ f j✝))
        else (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ 0)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [Category.comp_id, comp_zero, MonoidalPreadditive.tensor_zero, eqToHom_refl, tensor_id, if_true,
  dif_ctx_congr, Finset.sum_congr, Finset.mem_univ, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ 𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f j✝ = (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom
[PROOFSTEP]
simp only [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.lift fun j => biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
erw [biproduct.lift_π]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.π f j✝ ⊗ 𝟙 X =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero, Finset.sum_dite_eq',
  Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).inv = ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.ι (fun j => f j ⊗ X) j✝ ≫ biproduct.desc fun j => biproduct.ι f j ⊗ 𝟙 X) =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
simp only [biproduct.ι_desc, Preadditive.comp_sum, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp, Finset.sum_dite_eq,
  Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j = biproduct.π f j ⊗ 𝟙 X
[PROOFSTEP]
simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (biproduct.ι f j ⊗ 𝟙 X) ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j
[PROOFSTEP]
simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_tensor_id_assoc, biproduct.ι_π, dite_tensor, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ (biproduct.π f j ⊗ 𝟙 X) = biproduct.π (fun j => f j ⊗ X) j
[PROOFSTEP]
simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j => f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ⊗ 𝟙 X
[PROOFSTEP]
simp [rightDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
⊢ (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ (f j) X Y).symm
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ ((rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝ =
    (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ (f j) X Y).symm).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor, comp_tensor_id, tensorIso_hom, rightDistributor_hom,
  biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq',
  Finset.sum_const_zero, Finset.mem_univ, if_true]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => f j ⊗ X) j✝ ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ (∑ x : J,
      if h : x = j✝ then (biproduct.π f x ⊗ 𝟙 X) ≫ eqToHom (_ : f x ⊗ X = f j✝ ⊗ X) ⊗ 𝟙 Y
      else (biproduct.π f x ⊗ 𝟙 X) ≫ 0 ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [Category.comp_id, comp_tensor_id, eqToHom_refl, tensor_id, comp_zero, MonoidalPreadditive.zero_tensor,
  if_true, dif_ctx_congr, Finset.mem_univ, Finset.sum_congr, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ (biproduct.π f j✝ ⊗ 𝟙 X) ⊗ 𝟙 Y = (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [← tensor_id, associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
⊢ (leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ rightDistributor f Y) ≪≫
        (leftDistributor X fun j => f j ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ X (f j) Y).symm
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ ((leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => X ⊗ f j) Y).hom ≫
      biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝ =
    (α_ X (⨁ f) Y ≪≫
          (asIso (𝟙 X) ⊗ rightDistributor f Y) ≪≫
            (leftDistributor X fun j => f j ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ X (f j) Y).symm).hom ≫
      biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor, tensor_sum, comp_tensor_id, tensorIso_hom,
  leftDistributor_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π,
  Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ ∑ x : J,
      ((𝟙 X ⊗ biproduct.π f x) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => X ⊗ f j) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => X ⊗ f j) j✝ ⊗ 𝟙 Y) =
    ∑ x : J,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ biproduct.ι (fun j => f j ⊗ Y) x) ≫
          (𝟙 X ⊗ biproduct.π (fun j => f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite, dite_comp, tensor_dite,
  dite_tensor]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ (∑ x : J,
      if h : x = j✝ then (𝟙 X ⊗ biproduct.π f x) ≫ eqToHom (_ : X ⊗ f x = X ⊗ f j✝) ⊗ 𝟙 Y
      else (𝟙 X ⊗ biproduct.π f x) ≫ 0 ⊗ 𝟙 Y) =
    ∑ x : J,
      if h : x = j✝ then
        (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ eqToHom (_ : f x ⊗ Y = f j✝ ⊗ Y)) ≫ (α_ X (f j✝) Y).inv
      else (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ 0) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, Category.assoc, id_tensor_comp, comp_zero, zero_comp,
  MonoidalPreadditive.tensor_zero, MonoidalPreadditive.zero_tensor, comp_tensor_id, eqToHom_refl, tensor_id, if_true,
  dif_ctx_congr, Finset.sum_congr, Finset.mem_univ, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ (𝟙 X ⊗ biproduct.π f j✝) ⊗ 𝟙 Y = (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ biproduct.π f j✝ ⊗ 𝟙 Y) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (leftDistributor X f).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
⊢ (leftDistributor X f).inv ≫ g = (leftDistributor X f).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
[PROOFSTEP]
simp? [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
    dite_comp] says simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
[PROOFSTEP]
simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ (𝟙 X ⊗ biproduct.ι f j✝) ≫ g = (𝟙 X ⊗ biproduct.ι f j✝) ≫ h
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (leftDistributor Y f).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
⊢ g ≫ (leftDistributor Y f).hom = h ≫ (leftDistributor Y f).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝ =
    (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝
[PROOFSTEP]
simp? [leftDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
    comp_dite] says simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
    comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝ =
    (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝
[PROOFSTEP]
simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ g ≫ (𝟙 Y ⊗ biproduct.π f j✝) = h ≫ (𝟙 Y ⊗ biproduct.π f j✝)
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (α_ _ _ _).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
⊢ (α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ (𝟙 (X ⊗ Y) ⊗ biproduct.ι f j✝) ≫ (α_ X Y (⨁ f)).hom ≫ g = (𝟙 (X ⊗ Y) ⊗ biproduct.ι f j✝) ≫ (α_ X Y (⨁ f)).hom ≫ h
[PROOFSTEP]
simp_rw [← tensor_id, associator_naturality_assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (α_ _ _ _).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
⊢ g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (α_ Y Z (⨁ f)).inv) ≫ (𝟙 (Y ⊗ Z) ⊗ biproduct.π f j✝) = (h ≫ (α_ Y Z (⨁ f)).inv) ≫ (𝟙 (Y ⊗ Z) ⊗ biproduct.π f j✝)
[PROOFSTEP]
simp_rw [← tensor_id, Category.assoc, ← associator_inv_naturality, ← Category.assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (rightDistributor f X).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
⊢ (rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
[PROOFSTEP]
simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
    dite_comp] says simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
[PROOFSTEP]
simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ (biproduct.ι f j✝ ⊗ 𝟙 X) ≫ g = (biproduct.ι f j✝ ⊗ 𝟙 X) ≫ h
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (rightDistributor f Y).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
⊢ g ≫ (rightDistributor f Y).hom = h ≫ (rightDistributor f Y).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ (g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝ =
    (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝
[PROOFSTEP]
simp? [rightDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
    comp_dite] says simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
    comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ (g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝ =
    (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝
[PROOFSTEP]
simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ g ≫ (biproduct.π f j✝ ⊗ 𝟙 Y) = h ≫ (biproduct.π f j✝ ⊗ 𝟙 Y)
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (α_ _ _ _).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
⊢ (α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
j✝ : J
⊢ (biproduct.ι f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (⨁ f) X Y).inv ≫ g = (biproduct.ι f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (⨁ f) X Y).inv ≫ h
[PROOFSTEP]
simp_rw [← tensor_id, associator_inv_naturality_assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (α_ _ _ _).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
⊢ g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
j✝ : J
⊢ (g ≫ (α_ (⨁ f) Y Z).hom) ≫ (biproduct.π f j✝ ⊗ 𝟙 (Y ⊗ Z)) = (h ≫ (α_ (⨁ f) Y Z).hom) ≫ (biproduct.π f j✝ ⊗ 𝟙 (Y ⊗ Z))
[PROOFSTEP]
simp_rw [← tensor_id, Category.assoc, ← associator_naturality, ← Category.assoc, w]


[GOAL]
α β : Type u
S : Sieve β
hs : S ∈ GrothendieckTopology.sieves typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) S.arrows
hx : FamilyOfElements.Compatible x
γ : Type u
f : γ ⟶ β
h : S.arrows f
z : (Opposite.op γ).unop
⊢ (yoneda.obj α).map f.op (fun y => x (fun x => y) (_ : S.arrows fun x => y) PUnit.unit) z = x f h z
[PROOFSTEP]
convert congr_fun (hx (𝟙 _) (fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1
[GOAL]
α β : Type u
S : Sieve β
hs : S ∈ GrothendieckTopology.sieves typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) S.arrows
hx : FamilyOfElements.Compatible x
f : (yoneda.obj α).obj (Opposite.op β)
hf : (fun t => FamilyOfElements.IsAmalgamation x t) f
y : (Opposite.op β).unop
⊢ f y = x (fun x => y) (_ : S.arrows fun x => y) PUnit.unit
[PROOFSTEP]
convert congr_fun (hf _ (hs y)) PUnit.unit
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
⊢ S.map g.op (S.map g₁.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) β f₁ hf₁)) =
    S.map g.op (S.map g₂.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) γ f₂ hf₂))
[PROOFSTEP]
have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
  Classical.choose_spec hf₁ (g₁ <| g x) ▸ Classical.choose_spec hf₂ (g₂ <| g x) ▸ congr_fun h _
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂)
⊢ S.map g.op (S.map g₁.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) β f₁ hf₁)) =
    S.map g.op (S.map g₂.op ((fun β g hg => S.map (↾fun x => PUnit.unit).op (f (g (Classical.choose hg)))) γ f₂ hf₂))
[PROOFSTEP]
simp_rw [← FunctorToTypes.map_comp_apply, this, ← op_comp]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂)
⊢ S.map (g ≫ g₁ ≫ ↾fun x => PUnit.unit).op (f (f₂ (Classical.choose hf₂))) =
    S.map (g ≫ g₂ ≫ ↾fun x => PUnit.unit).op (f (f₂ (Classical.choose hf₂)))
[PROOFSTEP]
rfl
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
⊢ eval S α (typesGlue S hs α f) = f
[PROOFSTEP]
funext x
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
x : α
⊢ eval S α (typesGlue S hs α f) x = f x
[PROOFSTEP]
apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit)
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose (_ : ∃ x, ∀ (y : PUnit), y = x)))) = f x
[PROOFSTEP]
convert FunctorToTypes.map_id_apply S _
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ typesGlue S hs α (eval S α s) = s
[PROOFSTEP]
apply (hs.isSheafFor _ _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ ∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄, discretePresieve α f → S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
[PROOFSTEP]
intro β f hf
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
[PROOFSTEP]
apply (IsSheafFor.valid_glue _ _ _ hf).trans
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map (↾fun x => PUnit.unit).op (eval S α s (f (Classical.choose hf))) = S.map f.op s
[PROOFSTEP]
apply (FunctorToTypes.map_comp_apply _ _ _ _).symm.trans
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => f (Classical.choose hf)).op ≫ (↾fun x => PUnit.unit).op) s = S.map f.op s
[PROOFSTEP]
rw [← op_comp]
  --congr 2 -- Porting note: This tactic didn't work. Find an alternative.
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
[PROOFSTEP]
suffices ((↾fun _ ↦ PUnit.unit) ≫ ↾fun _ ↦ f (Classical.choose hf)) = f by rw [this]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
this : ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
⊢ S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
[PROOFSTEP]
rw [this]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
[PROOFSTEP]
funext x
[GOAL]
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) x = f x
[PROOFSTEP]
exact congr_arg f (Classical.choose_spec hf x).symm
[GOAL]
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ eval S β (S.map f.op s) x = eval S α s (f x)
[PROOFSTEP]
simp_rw [eval, ← FunctorToTypes.map_comp_apply, ← op_comp]
[GOAL]
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
[PROOFSTEP]
rfl
[GOAL]
S : SheafOfTypes typesGrothendieckTopology
⊢ { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } ≫
      { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } =
    𝟙 S
[PROOFSTEP]
ext1
[GOAL]
case w
S : SheafOfTypes typesGrothendieckTopology
⊢ ({ val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } ≫
        { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv }).val =
    (𝟙 S).val
[PROOFSTEP]
apply (equivYoneda S.1 S.2).hom_inv_id
[GOAL]
S : SheafOfTypes typesGrothendieckTopology
⊢ { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } ≫
      { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom } =
    𝟙 (yoneda'.obj (S.val.obj (op PUnit)))
[PROOFSTEP]
ext1
[GOAL]
case w
S : SheafOfTypes typesGrothendieckTopology
⊢ ({ val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).inv } ≫
        { val := (equivYoneda S.val (_ : IsSheaf typesGrothendieckTopology S.val)).hom }).val =
    (𝟙 (yoneda'.obj (S.val.obj (op PUnit)))).val
[PROOFSTEP]
apply (equivYoneda S.1 S.2).inv_hom_id
[GOAL]
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)
[PROOFSTEP]
refine' le_antisymm subcanonical_typesGrothendieckTopology (sInf_le _)
[GOAL]
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.toPrefunctor.obj
[PROOFSTEP]
refine' ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext _⟩
[GOAL]
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))).sieves = typesGrothendieckTopology.sieves
[PROOFSTEP]
funext α
[GOAL]
case h
α : Type u
⊢ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α =
    GrothendieckTopology.sieves typesGrothendieckTopology α
[PROOFSTEP]
ext S
[GOAL]
case h.h
α : Type u
S : Sieve α
⊢ S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α ↔
    S ∈ GrothendieckTopology.sieves typesGrothendieckTopology α
[PROOFSTEP]
refine' ⟨fun hs x => _, fun hs β f => isSheaf_yoneda' _ fun y => hs _⟩
[GOAL]
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
⊢ S.arrows fun x_1 => x
[PROOFSTEP]
by_contra hsx
[GOAL]
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
⊢ False
[PROOFSTEP]
have : (fun _ => ULift.up true) = fun _ => ULift.up false :=
  (hs PUnit fun _ => x).isSeparatedFor.ext fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y
[GOAL]
case h.h
α : Type u
S : Sieve α
hs : S ∈ GrothendieckTopology.sieves (Sheaf.finestTopologySingle (yoneda.obj (ULift Bool))) α
x : α
hsx : ¬S.arrows fun x_1 => x
this : (fun x => { down := true }) = fun x => { down := false }
⊢ False
[PROOFSTEP]
simp at this