mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) p)) (p.removeNth (update m i (x + y))) =
    (f (update m i x p)) (p.removeNth (update m i x)) + (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
cases i using Fin.succAboveCases p

Goal state after:
case x
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
x y : M p
⊢ (f (update m p (x + y) p)) (p.removeNth (update m p (x + y))) =
    (f (update m p x p)) (p.removeNth (update m p x)) + (f (update m p y p)) (p.removeNth (update m p y))

case p
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
j✝ : Fin n
x y : M (p.succAbove j✝)
⊢ (f (update m (p.succAbove j✝) (x + y) p)) (p.removeNth (update m (p.succAbove j✝) (x + y))) =
    (f (update m (p.succAbove j✝) x p)) (p.removeNth (update m (p.succAbove j✝) x)) +
      (f (update m (p.succAbove j✝) y p)) (p.removeNth (update m (p.succAbove j✝) y))
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x : R
y : M i
⊢ (f (update m i (x • y) p)) (p.removeNth (update m i (x • y))) = x • (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
cases i using Fin.succAboveCases p

Goal state after:
case x
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
x : R
y : M p
⊢ (f (update m p (x • y) p)) (p.removeNth (update m p (x • y))) = x • (f (update m p y p)) (p.removeNth (update m p y))

case p
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
x : R
j✝ : Fin n
y : M (p.succAbove j✝)
⊢ (f (update m (p.succAbove j✝) (x • y) p)) (p.removeNth (update m (p.succAbove j✝) (x • y))) =
    x • (f (update m (p.succAbove j✝) y p)) (p.removeNth (update m (p.succAbove j✝) y))
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
s : ↑(powersetCard I n)
i : I
⊢ i ∈ range ⇑(ofFinEmbEquiv.symm s) ↔ i ∈ s

Tactic:
simp [ofFinEmbEquiv_symm_apply]

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

Goal state before:
pp: case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]

Goal state after:
case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ (ι R) (f (y.pred ⋯).succ) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
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 : ∃ a ∈ ↑s, a ∈ ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t = 0

Tactic:
obtain ⟨i, his, hit⟩ := h

Goal state after:
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)
X✝ Y✝ : C
f : X✝ ⟶ X
g : X✝ ⟶ Y✝
x✝ : Mono g
φ : { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X
hφ :
  (Ext.mk₀ { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.f).comp (Ext.homEquiv₀.symm φ)
      ⋯ =
    Ext.mk₀ f
⊢ Ext.homEquiv₀.symm (g ≫ φ) = Ext.homEquiv₀.symm f

Tactic:
simpa using hφ

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq :
  (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) =
    (RingCat.Hom.hom (R'.map f)) ((RingCat.Hom.hom (α.app X)) r)
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x

Tactic:
← eq

Goal state after:
C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq :
  (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) =
    (RingCat.Hom.hom (R'.map f)) ((RingCat.Hom.hom (α.app X)) r)
⊢ (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limitPresheafOfModules F)).map f ≫
      { app := fun X ↦ limit.π (F ⋙ evaluation R X) j', naturality := ⋯ } =
    { app := fun X ↦ limit.π (F ⋙ evaluation R X) j, naturality := ⋯ } ≫ F.map f

Tactic:
by
        ext1 X
        simpa using (limit.w (F ⋙ evaluation R X) f).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
⊢ IsConnected C

Tactic:
have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
this : Nonempty C
⊢ IsConnected C
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✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ Z x x, True

Tactic:
obtain ⟨c, ⟨t, ht⟩⟩ := h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right))
        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ ∃ Z x x, True
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ ∃ c' t, (forget c).map t ≫ s = (forget c).map t ≫ s'

Tactic:
use mk (IsCofiltered.eqHom s s' ≫ x.hom)
      use homMk (IsCofiltered.eqHom s s') (by simp)
      simp only [forget_obj, mk_left, forget_map, homMk_left]
      rw [IsCofiltered.eq_condition]

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
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
c : Cocone (uncurry.obj F) := colimit.cocone (uncurry.obj F)
P : IsColimit c := colimit.isColimit (uncurry.obj F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
Q : (j : J) → IsColimit (G.obj j) := fun j ↦ colimit.isColimit (F.obj j)
Q' : IsColimit (coconeOfCoconeUncurry Q c)
Q'' : IsColimit (colimit.cocone (F ⋙ colim))
⊢ colimit (uncurry.obj F) ≅ colimit (F ⋙ colim)

Tactic:
exact IsColimit.coconePointUniqueUpToIso Q' Q''

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
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
j : J
k : K
⊢ (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j

Tactic:
by
  dsimp [limitFlipCompLimIsoLimitCompLim]
  simp [Equivalence.counit]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
⊢ x✝ ∈ F.obj U✝ ⊔ G.obj U✝ → x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)

Tactic:
rintro (h | h)

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
h : x✝ ∈ F.obj U✝
⊢ x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
h : x✝ ∈ G.obj U✝
⊢ x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ x✝¹ ⊗ₘ x✝ = x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝

Tactic:
by ext1; apply tensorHom_def

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
⊢ ∀ ⦃X : C⦄ (S : Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y),
    S ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton f} →
      (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}) →
        S.bind Ti ∈ {S | ∃ Y f, ∃ (_ : IsIso f), S = Presieve.singleton f}

Tactic:
rintro X S Ti ⟨Z, g, i, rfl⟩ hS
    rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩
    refine ⟨_, f ≫ g, ?_, ?_⟩
    · infer_instance
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): the next four lines were just "ext (W k)"
    apply funext
    intro W
    ext K
    constructor
    · rintro ⟨V, h, k, ⟨_⟩, hh, rfl⟩
      rw [hTi] at hh
      cases hh
      apply singleton.mk
    · rintro ⟨_⟩
      refine bind_comp g singleton.mk ?_
      rw [hTi]
      apply singleton.mk

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x y : FamilyOfElements P R
H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf
Z : C
f : Z ⟶ X
hf : R f
⊢ x f hf = y f hf

Tactic:
exact H f hf

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S

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

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
by
  have h := (le_generate R Y _ hf).choose_spec
  unfold FamilyOfElements.sieveExtend
  rw [t h.choose (𝟙 _) _ hf _]
  · simp
  · rw [id_comp]
    exact h.choose_spec.choose_spec.2

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t : Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)
ij : I × I
⊢ (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (secondMap P X π)) x)

Tactic:
simpa [firstMap, secondMap] using t ij.1 ij.2

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((equivShrink ((i : I) → P.obj (op (X i)))).symm
      ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x))
ij : I × I
⊢ (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (secondMap P X π)) x)

Tactic:
simpa [firstMap, secondMap] using t ij.1 ij.2

Goal state after:
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
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
⊢ (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
    (x.Compatible → ∃ t, x.IsAmalgamation t)

Tactic:
refine ⟨?_, ExistsUnique.exists ∘ h⟩

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
e : Subtype (Arrows.Compatible P g) ≃ Subtype (Arrows.Compatible P fun i ↦ g i ≫ inv f) :=
  { toFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, invFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
x✝¹ : P.obj (op Y)
x✝ : ι
⊢ ↑(((⇑e ∘ Arrows.toCompatible P g) ∘ ⇑(P.mapIso (asIso f).symm.op).toEquiv) x✝¹) x✝ =
    ↑(Arrows.toCompatible P (fun i ↦ g i ≫ inv f) x✝¹) x✝

Tactic:
simp [e]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i))
i₁ i₂ : I
Z : Over B
g₁ : Z ⟶ Y i₁
g₂ : Z ⟶ Y i₂
h : g₁ ≫ f i₁ = g₂ ≫ f i₂
⊢ (Over.map p).map g₁ ≫ (fun i ↦ (Over.map p).map (f i)) i₁ = (Over.map p).map g₂ ≫ (fun i ↦ (Over.map p).map (f i)) i₂

Tactic:
by simp only [← Functor.map_comp, h]

Goal state after:
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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ J.toSheafify P ≫ J.sheafifyLift η hQ = η

Tactic:
dsimp only [sheafifyLift, toSheafify]
  simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (sigmaIsoSigma α).inv) ⟨i, x⟩ = (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
    Category.comp_id]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
by
  refine .of_comp (ContinuousMap.continuous_toFun _)
    (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from
        ContinuousMap.continuous_toFun _)
      ?_
  suffices
    IsEmbedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by
    simpa [← coe_comp] using this
  rw [coe_comp]
  exact (isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp
      (pullback_map_isEmbedding (i₂ := 𝟙 Y) f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding
        (𝟙 _) rfl (by simp))

Goal state after:
X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B) (x : IsColimit c₁) (x : IsColimit c₂), Mono c₁.inl → Mono c₂.inl

Tactic:
intro c₁ c₂ hc₁ hc₂ _

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono c₁.inl
⊢ Mono c₂.inl
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
j : J
⊢ c.ι.app j ≫ (G.asEquivalence.unitIso.app c.pt).hom =
    ((Cocone.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c))).ι.app j

Tactic:
simp [e]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k ↦ X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ ∀ (i₁ : J),
    (c₁.inj i₁ ≫ Cofan.IsColimit.desc hc₁ fun i ↦ c.inj (ι i)) = (Cofan.mk c.pt fun i' ↦ c.inj (e i')).inj (Sum.inl i₁)

Tactic:
simp [e]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d

Tactic:
← reassoc_of% hY,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ c.inr ≫ d