mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ a ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with a.1 + a.2 = n, ↑(GradedMonoid.GMul.mul (r a.1) (r' a.2)) =
    ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with x.1 + x.2 = n, ↑(r x.1) * ↑(r' x.2)

Tactic:
SetLike.coe_gMul

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
by
  rw [mul_eq_dfinsuppSum]
  iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]; congr; ext
  dsimp only
  split_ifs with h
  · subst h
    rw [of_eq_same]
    rfl
  · rw [of_eq_of_ne _ _ _ (Ne.symm h)]
    rfl

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

Goal state before:
pp: V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∀ (d : ℕ), finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v

Tactic:
intro d

Goal state after:
V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
d : ℕ
⊢ finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑s).ncard = n

Tactic:
by
  rw [← coe_coe, Set.ncard_coe_finset, s.prop]

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s t : ↑(powersetCard α n)
⊢ s ≠ t ↔ ∃ a ∈ s, a ∉ t

Tactic:
by
  contrapose!
  rw [eq_iff_subset]
  rfl

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inr.zero
α : Type u_1
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α 0) = (Nat.card α).choose 0

pp: case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = (Nat.card α).choose (n + 1)

Tactic:
· simp [powersetCard]

Goal state after:
case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = (Nat.card α).choose (n + 1)
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

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 : ℕ), d = n + k → e = 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)
⊢ HasInjectiveDimensionLT X n

Tactic:
by
  suffices ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0 from
    HasInjectiveDimensionLT.mk (fun i hi Y e ↦ by
      obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi
      exact this e k rfl)
  intro d Y e k hd
  induction k generalizing d Y with
  | zero =>
    obtain rfl : d = n := by simpa using hd
    subsingleton
  | succ k hk =>
    let ⟨p⟩ := EnoughProjectives.presentation Y
    have h : (ShortComplex.mk _ _ (kernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_kernel p.f }
    have hd : (n + k) + 1 = d := by lia
    obtain ⟨x, rfl⟩ := Ext.contravariant_sequence_exact₃ h X e
      (by subst hd; apply Ext.eq_zero_of_projective) ((add_comm _ _).trans hd)
    simp [hk x rfl]

Goal state after:
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
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ιMulti R n) '' {a | range a ⊆ s}) = ⊤

Tactic:
apply LinearMap.map_injective (ker_subtype (⋀[R]^n M))

Goal state after:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ Submodule.map (⋀[R]^n M).subtype (span R (⇑(ιMulti R n) '' {a | range a ⊆ s})) = Submodule.map (⋀[R]^n M).subtype ⊤
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.span R (range (⇑(map n f) ∘ ⇑(ιMulti R n))) = Submodule.span R (range ⇑(ιMulti R n))

Tactic:
← LinearMap.coe_compAlternatingMap,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.span R (range ⇑((map n f).compAlternatingMap (ιMulti R n))) = Submodule.span R (range ⇑(ιMulti R n))
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat R
f : X ⟶ Y
g : Y ⟶ Z
⊢ localizedModuleMap S (f ≫ g) = localizedModuleMap S f ≫ localizedModuleMap S g

Tactic:
ext
    simp [IsLocalizedModule.map_comp' S _ (Y.localizedModuleMkLinearMap S)]

Goal state after:
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
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m = { app := fun X ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ }

Tactic:
ext1 X
    apply (hc X).uniq ((evaluation R X).mapCone s)
    intro j
    dsimp
    rw [← hm, comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: 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
X Y : J ⥤ C
j : J
⊢ (pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left } ≅
    (pair (X.obj j) (Y.obj j)).obj { as := WalkingPair.left }

Tactic:
exact Iso.refl _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: 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
X Y : J ⥤ C
j : J
⊢ (pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right } ≅
    (pair (X.obj j) (Y.obj j)).obj { as := WalkingPair.right }

Tactic:
exact Iso.refl _

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{(max u ?u.35) + 1}

Tactic:
haveI : PreservesLimitsOfShape (Discrete PEmpty) (colim : (C ⥤ _) ⥤ Type u) :=
    preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv') _

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{?u.66 + 1}) colim
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{(max u ?u.35) + 1}
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
by
  refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩
  obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty
  exact ⟨(fromInitialModel J).obj f.left, Set.mem_range_self _, ⟨f.hom⟩⟩

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✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)

Tactic:
intro d

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
hF : F.Final
d : D
⊢ ∃ c, Nonempty (d ⟶ F.obj c)
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' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
intro d

Goal state after:
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' t, s ≫ F.map t = s' ≫ F.map t
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, Nonempty (F.obj c ⟶ d)

Tactic:
intro d

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✝ : 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, Nonempty (F.obj c ⟶ d)
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✝ : 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} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
intro d

Goal state after:
case refine_2
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} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
intro d

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
⊢ ∀ {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c), ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
intro d

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
d : I s
⊢ ∀ {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d), ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
X : Cᵒᵖ
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m = (ModuleCat.Hom.hom (g₂.app X)) m

Tactic:
exact hf (ConcreteCategory.congr_hom ((evaluation R X ⋙ forget _).congr_map hg) m)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (freeObj F).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f

Tactic:
by
    dsimp
    ext x
    simpa using! NatTrans.naturality_apply φ f x

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    ιM (r • (((toPresheaf R).map f).app U).hom' m)

Tactic:
← (f.app U).hom.map_smul

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    ιM ((ModuleCat.Hom.hom (f.app U)) (r • m))
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₃₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
τ₀₁₃ : F₀₁ ⋙ F₁₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)))
      (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃)) ≫
        adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)) τ₀₁₃)) =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)))
      ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)) τ₀₁₃ ≫
          whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃) G₁₀))

Tactic:
simp [leftAdjointCompNatTrans, ← conjugateEquiv_whiskerLeft _ _ adj₀₁]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
⊢ S.bind Ti ∈ {R | Sieve.generate R ∈ J X}

Tactic:
by
    apply J.transitive hS
    intro Y f
    rintro ⟨Z, g, f, hf, rfl⟩
    rw [Sieve.pullback_comp]
    apply J.pullback_stable g
    apply J.superset_covering _ (hTi _ hf)
    rintro Y g ⟨W, h, g, hg, rfl⟩
    exact ⟨_, h, _, ⟨_, _, _, hf, hg, rfl⟩, by simp⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f →
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f →
    (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f

Tactic:
· rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩
    exact ofArrows.mk (Sigma.mk _ _)

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) (fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) f →
    (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) f
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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
funext x
  ext f
  constructor
  · rintro ⟨X, f₁, g₁, h₁, rfl⟩
    exact ⟨F.obj X, F.map f₁, g₁, ⟨X, f₁, 𝟙 _, h₁, by simp⟩, rfl⟩
  · rintro ⟨X, f₁, g₁, ⟨X', f₂, g₂, h₁, rfl⟩, rfl⟩
    exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
hF : (X : C) → IsInitial (F.obj X)
⊢ IsInitial F

Tactic:
refine evaluationJointlyReflectsColimits _
    fun X ↦ IsColimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
hF : (X : C) → IsInitial (F.obj X)
X : C
⊢ (Cocone.precompose ((empty D).emptyExt (empty (C ⥤ D) ⋙ (evaluation C D).obj X)).inv).obj (asEmptyCocone (F.obj X)) ≅
    ((evaluation C D).obj X).mapCocone (asEmptyCocone F)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ Presieve.FamilyOfElements.Compatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x) ↔
    (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

Tactic:
by
  rw [Presieve.pullbackCompatible_iff]
  constructor
  · intro t
    apply Limits.Types.limit_ext
    rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
    simpa [firstMap, secondMap] using t hf hg
  · intro t Y Z f g hf hg
    rw [Types.limit_ext_iff'] at t
    simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, (hom (↾fun f ↦ ↑f)) t = f✝) → S.arrows f✝

Tactic:
rintro ⟨⟨f, hf⟩, rfl⟩

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f : Opposite.unop (Opposite.op Y✝) ⟶ X
hf : S.arrows f
⊢ S.arrows ((hom (↾fun f ↦ ↑f)) ⟨f, hf⟩)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a.mk
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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ unop Z
hf✝ : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop)))).arrows f✝
⊢ Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := f✝ ≫ g.unop ≫ f.unop, hf := ⋯ } =
    Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := (f✝ ≫ g.unop) ≫ f.unop, hf := ⋯ }

Tactic:
congr 2

Goal state after:
case e_a.mk.e_6
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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ unop Z
hf✝ : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop)))).arrows f✝
⊢ f✝ ≫ g.unop ≫ f.unop = (f✝ ≫ g.unop) ≫ f.unop