mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
⊢ IsCyclic G

Tactic:
by
  classical
    cases nonempty_fintype G
    apply isCyclic_of_card_pow_eq_one_le
    intro n hn
    exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) _root_.id

Tactic:
by
  ext
  simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id,
    Finsupp.mapDomain_equiv_apply]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
⊢ rootsOfUnity k M = (powMonoidHom k).ker

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this : Function.Injective ⇑(toLin' M)
⊢ M * toMatrix' ↑(LinearEquiv.ofInjectiveEndo (toLin' M) this).symm = 1

Tactic:
refine Matrix.toLin'.injective (LinearMap.ext fun v => ?_)

Goal state after:
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this : Function.Injective ⇑(toLin' M)
v : n → K
⊢ (toLin' (M * toMatrix' ↑(LinearEquiv.ofInjectiveEndo (toLin' M) this).symm)) v = (toLin' 1) v
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

Tactic:
by
  rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
i j : n
g : GL n R
⊢ ↑((map f) g) i j = f (↑g i j)

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) =
    (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
rw [← map_sub, ← map_sub]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
⊢ mk ((head :: tail).dProdIndex fι) ((head :: tail).dProd fι fA) =
    (List.map (fun a ↦ mk (fι a) (fA a)) (head :: tail)).prod

Tactic:
simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (A i)
inst✝¹ : AddMonoid ι
inst✝ : GRing A
n : ℤ
⊢ (of A 0) ↑n = ↑n

Tactic:
by
  rfl

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x y : M
⊢ polar (⇑Q) x (a • y) = a • polar (⇑Q) x y

Tactic:
by
  rw [← IsScalarTower.algebraMap_smul R a y, polar_smul_right, algebraMap_smul]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' : QuadraticMap R M N
a : R
x : M
⊢ (⇑Q + ⇑Q') (a • x) = (a * a) • (⇑Q + ⇑Q') x

Tactic:
simp only [Pi.add_apply, smul_add, QuadraticMap.map_smul]

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
r : ↥(A 0)
r' : ⨁ (i : ι), ↥(A i)
j _x : ι
⊢ 0 + _x = j ↔ _x = j

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
⊢ f.uncurryLeft.curryLeft = f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case e_5.e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
x✝ : Fin k
⊢ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inl x✝)) = x

Tactic:
rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]

Goal state after:
case e_5.e_6.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
x✝ : Fin k
⊢ (s.orderEmbOfFin hk) x✝ ∈ s
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ ιMulti_family R m v s * ιMulti_family R n v t = 0

Tactic:
simp only [ιMulti_family, ιMulti_mul_ιMulti]

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
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ (ιMulti R (m + n)) (Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t))) = 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 : 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:
simp only [ιMulti_family, ιMulti_mul_ιMulti]

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)
h : Disjoint ↑s ↑t
⊢ (ιMulti R (m + n)) (Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t))) =
    Equiv.Perm.sign (permOfDisjoint h) • (ιMulti R (m + n)) (v ∘ ⇑(ofFinEmbEquiv.symm (disjUnion h)))
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 y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y

Tactic:
apply M.mk_eq
  obtain ⟨k, f, g, hfg⟩ := h
  use k, f, g
  simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg
  simp [hfg]

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)
⊢ m - m' ∈ (Hom.hom S.g).ker

Tactic:
simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]

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)
⊢ (Hom.hom S.g) m = (Hom.hom S.g) m'
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).compAlternatingMap (ιMulti R n))) = Submodule.span R (range ⇑(ιMulti R n))

Tactic:
map_comp_ιMulti,

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 ⇑((ιMulti R n).compLinearMap f)) = Submodule.span R (range ⇑(ιMulti R n))
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
ha : ⟨a, aS⟩ • h m = ⟨a, aS⟩ • 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
⊢ (zeroEquiv R M) ((ιMulti R 0) f) = 1

Tactic:
by
  simp [zeroEquiv]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝² : Closed A
inst✝¹ : BraidedCategory C
I : C
t : IsInitial I
inst✝ : MonoidalClosed C
⊢ default ≫ curry ((mulZero t).hom ≫ t.to B) = 𝟙 (I ⟹ B)

Tactic:
rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
    apply t.hom_ext

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

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 Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫ (((Functor.const J).obj (colimitPresheafOfModules F)).obj j).map f

Tactic:
dsimp
            erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]
            rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ F.obj Y ◁ β.app Y = F.obj X ◁ β.app X ≫ (tensorObj F G').map f

Tactic:
simp only [← id_tensorHom]
    apply (tensorHom (𝟙 F) β).naturality

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

Goal state before:
pp: case h.left.hr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ Zag c₁ X.right

Tactic:
exact Zag.of_hom X.hom.fst

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

Goal state before:
pp: C : Type u
inst✝³ : SmallCategory C
D : Type u
inst✝² : SmallCategory D
inst✝¹ : IsSifted C
F : C ⥤ D
inst✝ : F.Final
⊢ IsSifted D

Tactic:
have : PreservesFiniteProducts (colim : (D ⥤ Type u) ⥤ _) :=
    ⟨fun n ↦ preservesLimitsOfShape_of_natIso (Final.colimIso F)⟩
  exact of_colim_preservesFiniteProducts D

Goal state after:
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:
by
        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: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ F.Initial ↔
    (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
by
  refine ⟨fun hF => ?_, fun h => initial_of_exists_of_isCofiltered F h.1 h.2⟩
  obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance
  refine ⟨?_, ?_⟩
  · intro d
    obtain ⟨c, ⟨t⟩⟩ := h₁ (op d)
    exact ⟨c.unop, ⟨t.unop⟩⟩
  · intro d c s s'
    obtain ⟨c', t, ht⟩ := h₂ (Quiver.Hom.op s) (Quiver.Hom.op s')
    exact ⟨c'.unop, t.unop, Quiver.Hom.op_inj ht⟩

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

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (x✝ ⟶ F.obj (Classical.choice ⋯))

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩

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

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (F.obj (Classical.choice ⋯) ⟶ x✝)

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩

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 : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ RingCat.Hom.hom (cR.ι.app X) = (RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))

Tactic:
ext; dsimp; rw [← Cocone.w cR f]; dsimp

Goal state after:
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
M₁ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (λ_ M₁).inv.app X = (λ_ (M₁.obj X)).inv

Tactic:
by
  rfl

Goal state after:
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
M₁ M₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (β_ M₁ M₂).hom.app X = (β_ (M₁.obj X) (M₂.obj X)).hom

Tactic:
by
  rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ {S | ∃ R ∈ K.coverings X, R ≤ S.arrows} →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∃ R ∈ K.coverings Y, R ≤ S.arrows}) →
          R ∈ {S | ∃ R ∈ K.coverings X, R ≤ S.arrows}

Tactic:
rintro X S ⟨R', hR', RS⟩ R t

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ K.coverings X
RS : R' ≤ S.arrows
R : Sieve X
t : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∃ R ∈ K.coverings Y, R ≤ S.arrows}
⊢ R ∈ {S | ∃ R ∈ K.coverings X, R ≤ S.arrows}
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
by
  change S ∈ sInf (sieves '' s) X ↔ _
  simp

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⦄,
    S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
          R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
intro X S H₁ R H₂ Y f

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
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
Y : C
f : Y ⟶ X
⊢ ∃ Z g, R.arrows (g ≫ f)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: Y Z : Type u
g h : Y ⟶ Z
⊢ (equalizerIso g h).hom ≫ ↾Subtype.val = equalizer.ι g h

Tactic:
by
  rfl

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
⊢ x.Compatible → x.PullbackCompatible

Tactic:
intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ (ConcreteCategory.hom (P.map (pullback.fst f₁ f₂).op)) (x f₁ hf₁) =
    (ConcreteCategory.hom (P.map (pullback.snd f₁ f₂).op)) (x f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
f : P ⟶ Q
g : Q ⟶ U
⊢ (x.map f).map g = x.map (f ≫ g)

Tactic:
by
  rfl

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
Y : C
i : I
b : W ⟶ Z i
fac : b ≫ f i = a ≫ e.hom
⊢ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a

Tactic:
exact ⟨_, b, _, ⟨i⟩, by simp [reassoc_of% fac]⟩

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
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom ((J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
ConcreteCategory.comp_apply

Goal state after:
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S)))
      ((ConcreteCategory.hom ((J.diagram P X).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))