internlm/Lean-Github huggingface dataset:
Theorem: Profinite.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Theorem: Profinite.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals
Theorem: Profinite.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: Profinite.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: Profinite.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: Profinite.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: Profinite.Sigma.ιCompToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ Sigma.ι Z a ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a
Tactic:
simp [toFiniteCoproduct]
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.ιCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ ι Z a ≫ fromFiniteCoproduct Z = Sigma.ι Z a
Tactic:
simp [fromFiniteCoproduct]
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.ι_injective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
⊢ Function.Injective ↑(ι Z a)
Tactic:
intro x y hxy
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
x y : (forget Profinite).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y
Theorem: Profinite.finiteCoproduct.ι_injective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a : α
x y : (forget Profinite).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y
Tactic:
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.ι_jointly_surjective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
R : ↑(finiteCoproduct Z).toCompHaus.toTop
⊢ ∃ a r, R = ↑(ι Z a) r
Tactic:
exact ⟨R.fst, R.snd, rfl⟩
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
⊢ ∀ (x : (forget Profinite).obj (Z a)), ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
intro x
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Theorem: Profinite.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
change (ι Z a ≫ desc Z π) _ = _
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x
Theorem: Profinite.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x
Tactic:
simp only [ι_desc]
Proof state after:
no goals
Theorem: Profinite.finiteCoproduct.range_eq
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a b : α
h : a = b
⊢ Set.range ↑(ι Z a) = Set.range ↑(ι Z b)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Profinite.pullback.condition
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ fst f g ≫ f = snd f g ≫ g
Tactic:
ext ⟨_,h⟩
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
val✝ : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
Theorem: Profinite.pullback.condition
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
val✝ : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
Tactic:
exact h
Proof state after:
no goals
Theorem: Profinite.pullback.hom_ext
Proof state before:
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b
Tactic:
ext z
Proof state after:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget Profinite).obj Z
⊢ ↑a z = ↑b z
Theorem: Profinite.pullback.hom_ext
Proof state before:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget Profinite).obj Z
⊢ ↑a z = ↑b z
Tactic:
apply_fun (fun q => q z) at hfst hsnd
Proof state after:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
Theorem: Profinite.pullback.hom_ext
Proof state before:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
Tactic:
apply Subtype.ext
Proof state after:
case w.a
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
Theorem: Profinite.pullback.hom_ext
Proof state before:
case w.a
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
Tactic:
apply Prod.ext
Proof state after:
case w.a.h₁
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst

case w.a.h₂
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
Theorem: Profinite.pullback.hom_ext
Proof state before:
case w.a.h₁
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst
Tactic:
exact hfst
Proof state after:
no goals
Theorem: Profinite.pullback.hom_ext
Proof state before:
case w.a.h₂
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
Tactic:
exact hsnd
Proof state after:
no goals
Theorem: Profinite.toExplicitCompFromExcplict
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ toExplicit f i ≫ fromExplicit f i = 𝟙 (Limits.pullback f i)
Tactic:
refine' Limits.pullback.hom_ext (k := (toExplicit f i ≫ fromExplicit f i)) _ _
Proof state after:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst

case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd
Theorem: Profinite.toExplicitCompFromExcplict
Proof state before:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: Profinite.toExplicitCompFromExcplict
Proof state before:
case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd
Tactic:
rw [Category.id_comp, Category.assoc, fromExplicit, Limits.pullback.lift_snd,
  toExplicit, pullback.lift_snd]
Proof state after:
no goals
Theorem: Profinite.fromExcplictComptoExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.fst f i = 𝟙 (pullback f i) ≫ pullback.fst f i
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: Profinite.fromExcplictComptoExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.snd f i = 𝟙 (pullback f i) ≫ pullback.snd f i
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: Profinite.fst_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i = fromExplicit f i ≫ Limits.pullback.fst
Tactic:
dsimp [fromExplicit]
Proof state after:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst
Theorem: Profinite.fst_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
Proof state after:
no goals
Theorem: Profinite.snd_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.snd f i = fromExplicit f i ≫ Limits.pullback.snd
Tactic:
dsimp [fromExplicit]
Proof state after:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.snd f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.snd
Theorem: Profinite.snd_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.snd f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.snd
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
Proof state after:
no goals
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x ↔
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
constructor
Proof state after:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x →
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x

case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    FamilyOfElements.Compatible x
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x →
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂
Proof state after:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ let_fun this := (_ : HasPullback f₁ f₂);
  P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ let_fun this := (_ : HasPullback f₁ f₂);
  P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)
Tactic:
apply t
Proof state after:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Tactic:
have := hS hf₁ hf₂
Proof state after:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
this : HasPullback f₁ f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
this : HasPullback f₁ f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Tactic:
apply pullback.condition
Proof state after:
no goals
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    FamilyOfElements.Compatible x
Tactic:
intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
Proof state after:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Tactic:
have := hS hf₁ hf₂
Proof state after:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Theorem: CategoryTheory.Presieve.pullbackCompatible_iff'
Proof state before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Tactic:
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]
Proof state after:
no goals
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
    forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
Tactic:
ext fg
Proof state after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ ((forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    ((forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof state before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ ((forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    ((forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Tactic:
simp only [firstMap', secondMap', forkMap]
Proof state after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.fst ≫ P.map pullback.fst.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.snd ≫ P.map pullback.snd.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof state before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.fst ≫ P.map pullback.fst.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.snd ≫ P.map pullback.snd.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app]
Proof state after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof state before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Tactic:
have := hS fg.1.2.2 fg.2.2.2
Proof state after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof state before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]
Proof state after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ P.map (pullback.snd ≫ ↑fg.snd.snd).op a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝