mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').inverse.CommShift A

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
by
  simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle
    ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]
  exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ distinguishedTriangles

Tactic:
mem_distTriang_op_iff'

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:

Tactic:
Nat.card (rootsOfUnity k R) = Nat.card { x // x ∈ nthRoots k (1 : R) } :=
      Nat.card_congr (rootsOfUnityEquivNthRoots R k)
    _ = Fintype.card { x // x ∈ nthRoots k (1 : R) } := Nat.card_eq_fintype_card
    _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
    _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
    _ ≤ k := card_nthRoots k 1

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G✝
G : Type u_7
inst✝¹ : CommGroup G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
G' : Type u_8
inst✝ : CommGroup G'
ζ : ↥(rootsOfUnity (Nat.card G) G')
⊢ orderOf ↑↑ζ ∣ orderOf g

Tactic:
simpa only [orderOf_eq_card_of_forall_mem_zpowers hg, orderOf_dvd_iff_pow_eq_one,
      ← Units.val_pow_eq_pow_val, Units.val_eq_one] using! ζ.prop

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

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
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) ((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) a) = a

Tactic:
obtain ⟨⟨a, _⟩, ha⟩ := a

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
a inv✝ : R
val_inv✝ : a * inv✝ = 1
inv_val✝ : inv✝ * a = 1
ha : { val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ rootsOfUnity (Fintype.card n) R
⊢ (fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯)
      ((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) ⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩) =
    ⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * 0 = 1
hg : c = 0
⊢ a * d = 1

Tactic:
mul_zero,

Goal state after:
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - 0 = 1
hg : c = 0
⊢ a * d = 1
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
⊢ f a * f b + f b * f a = (f a + f b) * (f a + f b) - f a * f a - f b * f b

Tactic:
mul_add,

Goal state after:
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
⊢ f a * f b + f b * f a = (f a + f b) * f a + (f a + f b) * f b - f a * f a - f b * f b
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ (List.ofFn f).prod =
    mk ((List.finRange n).dProdIndex fun i ↦ (f i).fst) ((List.finRange n).dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
by
  rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
rw [mulHom_of_of]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (of A ai) ax * (of A bi) bx * (of A ci) cx = (of A ai) ax * ((of A bi) bx * (of A ci) cx)

Tactic:
simp_rw [of_mul_of]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ (of A (ai + bi + ci)) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul ax bx) cx) =
    (of A (ai + (bi + ci))) (GradedMonoid.GMul.mul ax (GradedMonoid.GMul.mul bx cx))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: 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
x x' y : M
⊢ polar (⇑Q) x y + polar (⇑Q) (-x') y = polar (⇑Q) x y + -polar (⇑Q) x' y

Tactic:
polar_neg_left

Goal state after:
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
x x' y : M
⊢ polar (⇑Q) x y + -polar (⇑Q) x' y = polar (⇑Q) x y + -polar (⇑Q) x' y
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case pos
ι : 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 x✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = ↑(r x✝¹) * ↑(r' x✝)

pp: case neg
ι : 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 x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0

Tactic:
· subst h
    rw [of_eq_same]
    rfl

Goal state after:
case neg
ι : 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 x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0
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✝¹ : HasAntidiagonal ι
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = ∑ ij ∈ antidiagonal n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
by
  classical
  rw [coe_mul_apply]
  apply Finset.sum_subset (fun _ ↦ by simp)
  aesop (erase simp not_and) (add simp not_and_or)

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.det ≠ 0

Tactic:
simpa using separatingLeft_iff_det_ne_zero

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 : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * 0 else 0) = 0

Tactic:
mul_zero,

Goal state after:
ι : 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 : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then 0 else 0) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ ¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0

Tactic:
by
  simp only [Anisotropic, not_forall, exists_prop, and_comm]

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * 0 else 0) = 0

Tactic:
mul_zero,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then 0 else 0) = 0
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case 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 l
⊢ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr x✝)) = y

Tactic:
rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]

Goal state after:
case 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 l
⊢ (sᶜ.orderEmbOfFin hl) x✝ ∉ s
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f 0) v

Tactic:
List.ofFn_zero,

Goal state after:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (liftAlternating f) [].prod = (f 0) v
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
j : J
x : ↑(F.obj j)
⊢ (r * s) • M.mk F ⟨j, x⟩ = r • s • M.mk F ⟨j, x⟩

Tactic:
simp [mul_smul]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N✝ : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
N : Type ?u.42
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ f = f'

Tactic:
rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (ιMulti_span R n M)]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N✝ : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
N : Type ?u.42
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ ∀ (s : ↑(range ⇑(ιMulti R n))), f ↑s = f' ↑s
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: 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 : ℕ
⊢ (Λ.chainComplexMap (𝟙 X)).f n = (𝟙 (Λ.chainComplex X)).f n

Tactic:
induction n with
  | zero => simp
  | succ n hn => obtain _ | n := n <;> simp [hn]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: 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 : ℕ
⊢ (Λ.chainComplexMap 0).f n = HomologicalComplex.Hom.f 0 n

Tactic:
induction n with
  | zero => simp
  | succ n hn => obtain _ | n := n <;> simp [hn]

Goal state after:
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 1 → M
⊢ (oneEquiv R M) ((ιMulti R 1) f) = f 0

Tactic:
by
  simp [oneEquiv]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
a b : colimit (constPUnitFunctor C)
⊢ a = b

Tactic:
by
    obtain ⟨c, ⟨⟩, rfl⟩ := jointly_surjective' a
    obtain ⟨d, ⟨⟩, rfl⟩ := jointly_surjective' b
    apply constant_of_preserves_morphisms (colimit.ι (constPUnitFunctor C) · PUnit.unit)
    exact fun c d f => colimit_sound f rfl

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

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
X Y : C ⥤ Type u
j : C
⊢ colimit.ι ((tensor (C ⥤ Type u)).obj (X, Y)) j ≫
      (HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
        colimit.pre (X ⊠ Y) (Functor.diag C) ≫
          (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom =
    colimit.ι ((tensor (C ⥤ Type u)).obj (X, Y)) j ≫ CartesianMonoidalCategory.prodComparison colim X Y

Tactic:
dsimp [externalProductBifunctor, CartesianMonoidalCategory.prodComparison,
    externalProductBifunctorCurried, externalProduct]

Goal state after:
C : Type u
inst✝ : SmallCategory C
X Y : C ⥤ Type u
j : C
⊢ colimit.ι (X ⊗ Y) j ≫
      (HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
        colimit.pre (uncurry.obj ((((whiskeringLeft₂ (Type u)).obj X).obj Y).obj (curriedTensor (Type u))))
            (Functor.diag C) ≫
          (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom =
    colimit.ι (X ⊗ Y) j ≫ lift (colimMap (fst X Y)) (colimMap (snd X Y))
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)⟩

Goal state after:
C : Type u
inst✝³ : SmallCategory C
D : Type u
inst✝² : SmallCategory D
inst✝¹ : IsSifted C
F : C ⥤ D
inst✝ : F.Final
this : PreservesFiniteProducts colim
⊢ IsSifted D
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
inst✝ : IsFilteredOrEmpty C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ ∃ t, s ≫ (forget c).map t = s' ≫ (forget c).map t

Tactic:
use homMk (IsFiltered.coeqHom s s') (by simp)

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ s ≫ (forget c).map (homMk (IsFiltered.coeqHom s s') ⋯) = s' ≫ (forget c).map (homMk (IsFiltered.coeqHom s s') ⋯)
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
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫
      (G.obj c₁.pt).map (c₂.ι.app j.2) ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom =
    c₃.ι.app j

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv]
  simp

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:
obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty

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
f : StructuredArrow d F
⊢ ∃ c, Nonempty (d ⟶ F.obj c)
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

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

Tactic:
exact ⟨P.FullSubcategory, small_of_surjective (f := G.obj)
      (by rintro ⟨_, Y, _, rfl⟩; exact ⟨Y, rfl⟩), inferInstance, inferInstance, P.ι,
      Functor.final_of_comp_full_faithful' G P.ι ⟩

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

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

Tactic:
use Classical.choice IsFiltered.nonempty
    exact ⟨Discrete.eqToHom (by simp)⟩

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
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom).app X✝ = ((ρ_ X✝¹).hom ≫ x✝).app X✝

Tactic:
apply rightUnitor_naturality

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S.arrows f ∨ R.arrows f → ∀ (g : Z ⟶ Y), S.arrows (g ≫ f) ∨ R.arrows (g ≫ f)

Tactic:
rintro _ _ _ (h | h) g <;> simp [h]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
⊢ GaloisInsertion (pushforward f) (pullback f)

Tactic:
apply (galoisConnection f).toGaloisInsertion
  intro S Z g hg
  exact ⟨g ≫ section_ f, by simpa⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
Y : C
u : Y ⟶ X
hu : R u
⊢ (ConcreteCategory.hom (f.app (op Y))) ((ConcreteCategory.hom (P.map u.op)) t) =
    (ConcreteCategory.hom (f.app (op Y))) (x u hu)

Tactic:
simpa using ht _ hu

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPullback F S).arrows (F.preimage ((F.objObjPreimageIso Y).hom ≫ f)) ∧
    f = (F.objObjPreimageIso Y).inv ≫ F.map (F.preimage ((F.objObjPreimageIso Y).hom ≫ f))

Tactic:
simpa using hf

Goal state after: