mathlib-initiative/mathlib-tactics huggingface dataset:
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
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t =
    Equiv.Perm.sign (permOfDisjoint h) • ιMulti_family R (m + n) v (disjUnion h)

Tactic:
by
  simp only [ιMulti_family, ιMulti_mul_ιMulti]
  rw [← AlternatingMap.map_perm, permOfDisjoint]
  congr
  ext i
  let e := powersetCard.orderIsoOfFin (powersetCard.disjUnion h)
  change _ = v (e (e.symm _))
  by_cases! hi : i < m
  · rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_castAdd]
    aesop
  · rw [← Fin.natAdd_subNat_cast hi, Fin.append_right, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_natAdd]
    aesop

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
n : ↑S.X₁
hnm : (Hom.hom S.f) n = m - m'
⊢ m ∈ span R (range u)

Tactic:
have hn : n ∈ span R (range v) := hv mem_top

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
n : ↑S.X₁
hnm : (Hom.hom S.f) n = m - m'
hn : n ∈ span R (range v)
⊢ m ∈ span R (range u)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (𝟙 X)).f 0 = (𝟙 (Λ.chainComplex X)).f 0
⊢ (Λ.chainComplexMap (𝟙 X)).f (0 + 1) = (𝟙 (Λ.chainComplex X)).f (0 + 1)

pp: case succ.succ
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (𝟙 X)).f (n + 1) = (𝟙 (Λ.chainComplex X)).f (n + 1)
⊢ (Λ.chainComplexMap (𝟙 X)).f (n + 1 + 1) = (𝟙 (Λ.chainComplex X)).f (n + 1 + 1)

Tactic:
<;>

Goal state after:
case succ.zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (𝟙 X)).f 0 = (𝟙 (Λ.chainComplex X)).f 0
⊢ (Λ.chainComplexMap (𝟙 X)).f (0 + 1) = (𝟙 (Λ.chainComplex X)).f (0 + 1)

case succ.succ
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (𝟙 X)).f (n + 1) = (𝟙 (Λ.chainComplex X)).f (n + 1)
⊢ (Λ.chainComplexMap (𝟙 X)).f (n + 1 + 1) = (𝟙 (Λ.chainComplex X)).f (n + 1 + 1)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.zero
A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
hn : (Λ.chainComplexMap 0).f 0 = HomologicalComplex.Hom.f 0 0
⊢ (Λ.chainComplexMap 0).f (0 + 1) = HomologicalComplex.Hom.f 0 (0 + 1)

pp: case succ.succ
A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
n : ℕ
hn : (Λ.chainComplexMap 0).f (n + 1) = HomologicalComplex.Hom.f 0 (n + 1)
⊢ (Λ.chainComplexMap 0).f (n + 1 + 1) = HomologicalComplex.Hom.f 0 (n + 1 + 1)

Tactic:
<;>

Goal state after:
case succ.zero
A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
hn : (Λ.chainComplexMap 0).f 0 = HomologicalComplex.Hom.f 0 0
⊢ (Λ.chainComplexMap 0).f (0 + 1) = HomologicalComplex.Hom.f 0 (0 + 1)

case succ.succ
A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
n : ℕ
hn : (Λ.chainComplexMap 0).f (n + 1) = HomologicalComplex.Hom.f 0 (n + 1)
⊢ (Λ.chainComplexMap 0).f (n + 1 + 1) = HomologicalComplex.Hom.f 0 (n + 1 + 1)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case h_fst
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y))

pp: case h_snd
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y))

Tactic:
<;>

Goal state after:
case h_fst
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y))

case h_snd
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y))
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} J₁
inst✝³ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝² : Category.{v_3, u_3} C₁
inst✝¹ : Category.{v_4, u_4} C₂
inst✝ : Category.{v_5, u_5} C
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cone K₁
c₂ : Cone K₂
⊢ ∀ ⦃X Y : J₁ × J₂⦄ (f : X ⟶ Y),
    (((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map f ≫
        match Y with
        | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) =
      (match X with
        | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
        (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map f

Tactic:
rintro ⟨j₁, j₂⟩ ⟨k₁, k₂⟩ ⟨f₁, f₂⟩
        dsimp
        simp only [assoc, id_comp, NatTrans.naturality_assoc,
          ← Functor.map_comp,
          ← NatTrans.comp_app_assoc, c₁.w, c₂.w]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : Cᵒᵖ
t : op d ⟶ F.op.obj c
⊢ ∃ c, Nonempty (F.obj c ⟶ d)

Tactic:
exact ⟨c.unop, ⟨t.unop⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: case refine_2
J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesColimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι := { app := fun k ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
j₂ : J₂
this :
  (G.obj (K₁.obj j₁)).map (c₂.ι.app j₂) ≫
      (P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun k ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } =
    (G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)
⊢ (Q₀.obj j₁).ι.app j₂ ≫ (G.map (c₁.ι.app j₁)).app c₂.pt = (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s

Tactic:
simp only [Functor.mapCocone_pt,
            Functor.mapCocone_ι_app, NatTrans.naturality, this, Q₀, s]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
⊢ R ∈ J X

Tactic:
apply J.transitive sjx R fun Y f hf => _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve Y
T : Presieve X
hle : R ≤ pullback f T
Z : C
g : Z ⟶ Y
hg : R g
⊢ T (g ≫ f)

Tactic:
exact hle _ _ hg

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

Goal state before:
pp: case inl
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✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : S.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)

pp: case inr
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✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)

Tactic:
<;>

Goal state after:
case inl
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✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : S.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)

case inr
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✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.SieveCompatible → x.Compatible

Tactic:
intro h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k
    simp_rw [← h f₁ g₁ h₁, ← h f₂ g₂ h₂]
    congr

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)

Tactic:
Sieve.pullback_apply,

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows ((h ≫ pullback.snd g f) ≫ f)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ (↑(eqv π)).IsAmalgamation ↑(eqv' f₁)

pp: case mpr.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ (↑(eqv π)).IsAmalgamation ↑(eqv' f₂)

Tactic:
<;>

Goal state after:
case mpr.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ (↑(eqv π)).IsAmalgamation ↑(eqv' f₁)

case mpr.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ (↑(eqv π)).IsAmalgamation ↑(eqv' f₂)
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
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
⊢ ∀ (s : Cone (S.index P).multicospan) (m : s.pt ⟶ (S.multifork P).pt),
    (∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = s.π.app j) →
      m = hP.amalgamate S (fun x ↦ Multifork.ι s x) ⋯

Tactic:
rintro (E : Multifork _) m hm

Goal state after:
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)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
⊢ m = hP.amalgamate S (fun x ↦ E.ι x) ⋯
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫
      Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯ ≫
        colimit.ι (J.diagram P (unop Y)) (op ⊤) =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj (op ⊤))).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram P (unop Y)) ((J.pullback f.unop).op.obj (op ⊤))

Tactic:
dsimp only [Functor.op, unop_op]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫
      Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯ ≫
        colimit.ι (J.diagram P (unop Y)) (op ⊤) =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop X))) (fun I ↦ P.map I.f.op) ⋯ ≫
      Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: 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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (II.r.g₁ ≫ II.fst.toMiddleHom) ≫ { Y := II.fst.middle, f := II.fst.fromMiddleHom, hf := ⋯ }.f =
    (II.r.g₂ ≫ II.snd.toMiddleHom) ≫ { Y := II.snd.middle, f := II.snd.fromMiddleHom, hf := ⋯ }.f

Tactic:
simpa only [Category.assoc, Cover.Arrow.middle_spec] using II.r.w

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ E.ι.app j ≫ hE.desc ((sheafToPresheaf J D).mapCocone S) = (S.ι.app j).hom

Tactic:
hE.fac

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ ((sheafToPresheaf J D).mapCocone S).ι.app j = (S.ι.app j).hom
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F → HasLimit (F ⋙ forget)

pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit (F ⋙ forget) → HasLimit F

Tactic:
<;>

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F → HasLimit (F ⋙ forget)

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit (F ⋙ forget) → HasLimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F → HasColimit (F ⋙ forget)

pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit (F ⋙ forget) → HasColimit F

Tactic:
<;>

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F → HasColimit (F ⋙ forget)

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit (F ⋙ forget) → HasColimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.left } =
    S.π.app { as := WalkingPair.left }

pp: case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.right } =
    S.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.left } =
    S.π.app { as := WalkingPair.left }

case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.right } =
    S.π.app { as := WalkingPair.right }