mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a : CliffordAlgebra Q
ha : a ∈ ((ι Q).range ^ 2) ^ k
b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
⊢ motive (a * b) ⋯

Tactic:
| mem_mul_mem a ha b hb =>

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(ι R).range
hu : (List.ofFn fun i ↦ ↑(f i)).prod ∈ ↑(ι R).range ^ n
i : Fin n
v : M
hv : (ι R) v = ↑(f i)
⊢ (ι R) (ιInv ((ι R) v)) = (ι R) v

Tactic:
ι_leftInverse

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(ι R).range
hu : (List.ofFn fun i ↦ ↑(f i)).prod ∈ ↑(ι R).range ^ n
i : Fin n
v : M
hv : (ι R) v = ↑(f i)
⊢ (ι R) v = (ι R) v
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x : ↑(M F)
⊢ ↑(M F)

Tactic:
refine Quot.lift (colimitSMulAux F r) ?_ x
    intro x y h
    apply colimitSMulAux_eq_of_rel
    apply Types.FilteredColimit.rel_of_colimitTypeRel
    exact h

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e = 0

Tactic:
← e.comp_mk₀_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e.comp (Ext.mk₀ (𝟙 X)) ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
⊢ ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0

Tactic:
intro d Y e k hd

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
e : Ext Y X d
k : ℕ
hd : d = n + k
⊢ e = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
this : (ExteriorAlgebra.ιMulti R n) (v ∘ α) = 0
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
by simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso (CartesianMonoidalCategory.prodComparison colim X Y)

Tactic:
← factorization_prodComparison_colim

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso
    ((HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
      colimit.pre (X ⊠ Y) (Functor.diag C) ≫
        (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PreservesLimit (empty (C ⥤ Type u)) colim

Tactic:
apply preservesTerminal_of_iso

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ colim.obj (⊤_ C ⥤ Type u) ≅ ⊤_ Type u
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
⊢ Function.Surjective G.obj

Tactic:
rintro ⟨_, Y, _, rfl⟩

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
Y : FinalModel C₀
⊢ ∃ a, G.obj a = { obj := (fromFinalModel C₀).obj Y, property := ⋯ }
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
this : IsFilteredOrEmpty (AsSmall C)
d : D
c : C
s s' : d ⟶ F.obj c
c' : AsSmall C
t : { down := c } ⟶ c'
ht : AsSmall.up.map s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t = AsSmall.up.map s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
exact ⟨AsSmall.down.obj c', AsSmall.down.map t, s₂.functor.map_injective (by simp_all [s₁, s₂])⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
⊢ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    s.π.app p.1 ≫ (D.obj p.1).π.app p.2 ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2

Tactic:
rcases p with ⟨j, k⟩

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    s.π.app (j, k).1 ≫ (D.obj (j, k).1).π.app (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2 ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1 ≫ 𝟙 s.pt

Tactic:
rcases p with ⟨j, k⟩

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2 ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    (D.obj (j, k).1).ι.app (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
by
  obtain ⟨τ₀₁₂, rfl⟩ := (conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).surjective τ₀₁₂
  obtain ⟨τ₀₂₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)).surjective τ₀₂₃
  apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective
  simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, leftAdjointCompNatTrans]
  rw [← cancel_mono (associator G₃₂ G₂₁ G₁₀).hom, Category.assoc, Category.assoc,
    Iso.inv_hom_id, Category.comp_id, ← conjugateEquiv_associator_hom adj₀₁ adj₁₂ adj₂₃,
    ← conjugateEquiv_whiskerRight _ _ adj₂₃, conjugateEquiv_comp, Iso.hom_inv_id_assoc,
    conjugateEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ {⊤}
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R ∈ {⊤}

Tactic:
Set.mem_singleton_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R ∈ {⊤}
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ (Presieve.ofArrows (fun i ↦ Limits.pullback (g i) f) fun x ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X

Tactic:
exact mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
i : s.pt
⊢ (hom g) ((hom s.ι) i) = (hom h) ((hom s.ι) i)

Tactic:
apply congr_hom s.condition i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
i : s.pt
⊢ (hom g) ((hom s.ι) i) = (hom h) ((hom s.ι) i)

Tactic:
apply congr_hom s.condition i

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
⊢ (ConcreteCategory.hom (↾fun g ↦ g₁ ≫ g)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) =
    (ConcreteCategory.hom (↾fun g ↦ g₂ ≫ g)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂)

Tactic:
dsimp [yonedaFamilyOfElements_fromCocone]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }

Tactic:
let F : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk (g₂ ≫ f₂) : Over X) := Over.homMk (𝟙 Z)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h : ⟨Z, v⟩ ∈ {⟨Y, u⟩}
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry

Tactic:
Set.mem_singleton_iff,

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h : ⟨Z, v⟩ = ⟨Y, u⟩
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝¹ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
R : Sieve Y
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : ∃ g, g ≫ f = f✝ ∧ R.arrows g
h : Z✝ ⟶ Y✝
j : Y✝ ⟶ Y
k : j ≫ f = f✝
z : R.arrows j
⊢ R.arrows (h ≫ j)

Tactic:
simp [z]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
dsimp [IsSheaf]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf K.toGrothendieck (P ⋙ coyoneda.obj (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
← (S.multifork P).w (WalkingMulticospan.Hom.fst b),

Goal state after:
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫
      (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b)) ≫
        (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
· obtain ⟨t, ht₁, ht₂⟩ := h _ hx.familyOfElements_compatible
    refine ⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩
    · rw [ht₁ _ (ofArrows.mk i), hx.familyOfElements_ofArrows_mk]
    · rw [ht', hx.familyOfElements_ofArrows_mk]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x✝ : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) x = y i
right✝ :
  ∀ (y_1 : (fun X ↦ X) (P.obj (op B))),
    (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = y i) y_1 → y_1 = x
⊢ ∃ a, Arrows.toCompatible P π a = ⟨y, hy⟩

Tactic:
exact ⟨x, by ext; apply hx⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y))

Tactic:
convert! e using 1

Goal state after:
case e'_2
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    ↑(x.refine h1) i

case e'_3
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y)) =
    ↑(y.refine h2) i
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
⊢ l₁ = l₂

Tactic:
by
  ext U s
  apply (h _ s.prop).isSeparatedFor.ext
  rintro V i hi
  dsimp
  rw [← dsimp% l₁.naturality_apply, ← dsimp% l₂.naturality_apply]
  exact ConcreteCategory.congr_hom (congr_app e <| op V) ⟨_, hi⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
hT : t.Compatible
Z Y : C
f : Z ⟶ Y
g : Y ⟶ X
hg : U.arrows g
hf : (B hg).arrows f
⊢ (ConcreteCategory.hom (P.map (f ≫ g).op)) (hU.amalgamate t hT) = s (f ≫ g) ⋯

Tactic:
rw [op_comp, Functor.map_comp, comp_apply, Presieve.IsSheafFor.valid_glue _ _ _ hg]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
hT : t.Compatible
Z Y : C
f : Z ⟶ Y
g : Y ⟶ X
hg : U.arrows g
hf : (B hg).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) (t g hg) = s (f ≫ g) ⋯