internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫
      (PreservesProduct.iso F fun a => (Z a).op).inv ≫
        F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) ≫ F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f
Tactic:
rw [← Functor.map_comp, ← op_inv, ← op_comp, ← ha, v.snd hS, piCompInvdesc,
  ← Functor.map_comp, CoprodToProdInvComp.ι, @PreservesProduct.isoInvCompMap _ _ _ _ F _ _ _ _ (_) a]
Proof state after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫ Pi.π (fun j => F.obj (Z j).op) a = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫ Pi.π (fun j => F.obj (Z j).op) a = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Tactic:
simp only [comparisoninv, op_id, limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
Proof state after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op) = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op) = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Tactic:
erw [F.map_id, Category.comp_id]
Proof state after:
no goals
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Presieve.IsSheafFor F S
Tactic:
refine' (Equalizer.Presieve.sheaf_condition' F <| isPullbackSieve_ExtensiveSieve hS).2 _
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap F fun {Y} {f} => S f)
        (_ :
          (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
            (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.secondMap' F
                (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g))))
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap F fun {Y} {f} => S f)
        (_ :
          (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
            (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.secondMap' F
                (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g))))
Tactic:
rw [Limits.Types.type_equalizer_iff_unique]
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : Equalizer.FirstObj F fun {Y} {f} => S f),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : Equalizer.FirstObj F fun {Y} {f} => S f),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
dsimp [Equalizer.FirstObj]
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : ∏ fun f => F.obj f.fst.op),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
exact isSheafForDagurSieveIsIsoFork hS hF
Proof state after:
no goals
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
⊢ ∀ (y : ∏ fun f => F.obj f.fst.op),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
intro y _
Proof state after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
refine' ⟨inv (Equalizer.forkMap F S) y, _, fun y₁ hy₁ => _⟩
Proof state after:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) (inv (Equalizer.forkMap F S) y)

case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) y₁
⊢ y₁ = inv (Equalizer.forkMap F S) y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) (inv (Equalizer.forkMap F S) y)
Tactic:
change (inv (Equalizer.forkMap F S) ≫ (Equalizer.forkMap F S)) y = y
Proof state after:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (inv (Equalizer.forkMap F S) ≫ Equalizer.forkMap F S) y = y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (inv (Equalizer.forkMap F S) ≫ Equalizer.forkMap F S) y = y
Tactic:
rw [IsIso.inv_hom_id, types_id_apply]
Proof state after:
no goals
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) y₁
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
replace hy₁ := congr_arg (inv (Equalizer.forkMap F S)) hy₁
Proof state after:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : inv (Equalizer.forkMap F S) (Equalizer.forkMap F (fun {Y} {f} => S f) y₁) = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : inv (Equalizer.forkMap F S) (Equalizer.forkMap F (fun {Y} {f} => S f) y₁) = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
change ((Equalizer.forkMap F S) ≫ inv (Equalizer.forkMap F S)) _ = _ at hy₁
Proof state after:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (Equalizer.forkMap F S ≫ inv (Equalizer.forkMap F S)) y₁ = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Theorem: CategoryTheory.isSheafForExtensiveSieve
Proof state before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (Equalizer.forkMap F S ≫ inv (Equalizer.forkMap F S)) y₁ = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
rwa [IsIso.hom_inv_id, types_id_apply] at hy₁
Proof state after:
no goals
Theorem: Profinite.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let ζ := finiteCoproduct.desc _ (fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a )
Proof state after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: Profinite.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let σ := finiteCoproduct.desc _ ((fun a => pullback.fst f (π a)))
Proof state after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: Profinite.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let β := finiteCoproduct.desc _ π
Proof state after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: Profinite.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
have comm : ζ ≫ β = σ ≫ f := by
   refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
   simp [← Category.assoc, finiteCoproduct.ι_desc, pullback.condition]
Proof state after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: Profinite.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
intro R₁ R₂ hR
Proof state after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
R₁ R₂ : (forget Profinite).obj (finiteCoproduct fun a => pullback f (π a))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
⊢ R₁ = R₂