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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        G.map (f₁.hom.app ((shiftFunctor C a).obj X)) ≫
          G.map ((shiftFunctor D b).map (e₁.hom.app X)) ≫
            G.map ((shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).hom.app (F.obj X)) ≫
                f₂.hom.app ((shiftFunctor D a).obj (F.obj X)) ≫
                  (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫ (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))

Tactic:
slice_rhs 5 6 => rw [← G.map_comp, Iso.inv_hom_id_app]

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        G.map (f₁.hom.app ((shiftFunctor C a).obj X)) ≫
          G.map ((shiftFunctor D b).map (e₁.hom.app X)) ≫
            ((G.map (𝟙 ((shiftFunctor D a ⋙ shiftFunctor D b).obj (F.obj X))) ≫
                  f₂.hom.app ((shiftFunctor D a).obj (F.obj X))) ≫
                (shiftFunctor C b).map (e₂.hom.app (F.obj X))) ≫
              (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (opShiftFunctorEquivalence C p).unitIso.hom.app X =
    (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
      ((shiftFunctor C n).map ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op

Tactic:
by
  dsimp [opShiftFunctorEquivalence]
  simp only [shiftFunctorAdd'_op_inv_app _ n m p (by lia) _ _ _ (add_neg_cancel n)
    (add_neg_cancel m) (add_neg_cancel p), shiftFunctor_op_map _ m (-m),
    Category.assoc, Iso.inv_hom_id_app_assoc]
  erw [Functor.map_id, Functor.map_id, Functor.map_id, Functor.map_id,
    id_comp, id_comp, id_comp, comp_id, comp_id]
  dsimp
  rw [comp_id, shiftFunctorCompIsoId_add'_hom_app _ _ _ _ _ _
    (neg_add_cancel m) (neg_add_cancel n) (neg_add_cancel p) h]
  dsimp
  rw [Category.assoc, Category.assoc]
  rfl

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

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Fintype n
this : Fintype m
h : ∀ (v : n → R), M *ᵥ v = 0 → v = 0
w : n → R
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ (M *ᵥ w) i = 0 i

Tactic:
classical simpa using hw <| Pi.single i 1

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
⊢ rootsOfUnity k M ≤ rootsOfUnity (k * d) M

Tactic:
intro ζ h

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mp
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
⊢ M.det = 0

Tactic:
contrapose! hv

Goal state after:
case mp
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
mul_eq : M *ᵥ v = 0
hv : M.det ≠ 0
⊢ v = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, True ∧ 0 < v b
⊢ ∃ b, True ∧ 0 < (-1 • v) b

Tactic:
true_and

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
⊢ ↑((fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 *
          (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i2)
      i j =
    ↑((fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i2 *
          (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1)
      i j

Tactic:
simp [apply_dite, diag2n_coe]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
⊢ (if i2 = i₀ then if i1 = i₀ then 1 else diagonal fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1
      else
        if i1 = i₀ then diagonal fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1
        else
          diagonal fun i ↦
            if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
            else
              if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else if i = i₀ then (D i1)⁻¹ * (D i2)⁻¹ else (D i2)⁻¹
              else if i = i1 then D i1 else if i = i₀ then (D i1)⁻¹ else 1)
      i j =
    (if i1 = i₀ then if i2 = i₀ then 1 else diagonal fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1
      else
        if i2 = i₀ then diagonal fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1
        else
          diagonal fun i ↦
            if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
            else
              if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else if i = i₀ then (D i2)⁻¹ * (D i1)⁻¹ else (D i1)⁻¹
              else if i = i2 then D i2 else if i = i₀ then (D i2)⁻¹ else 1)
      i j
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj

Tactic:
simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ F ((of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = F ((of A i) ai) * F ((of A j) aj)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(n✝ + 1) ∈ A 0

Tactic:
rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)

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

Goal state before:
pp: case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j : Fin (d + 1)
⊢ ∀ ⦃j_1 : Fin (d + 1)⦄, j ≠ j_1 → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j j_1

Tactic:
i

Goal state after:
case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
⊢ j ≠ i → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j i
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
x✝ : β
⊢ x✝ ∈ ↑(map n f s) ↔ x✝ ∈ ⇑f '' ↑s

Tactic:
simp [mem_map_iff_mem_range]

Goal state after:
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₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (x y : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (x + y)) t) =
      (f fun t ↦ Sum.rec u (update m i x) t) + f fun t ↦ Sum.rec u (update m i y) t

Tactic:
by let := Classical.decEq ι; simp

Goal state after:
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₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (c : R) (x : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (c • x)) t) = c • f fun t ↦ Sum.rec u (update m i x) t

Tactic:
by let := Classical.decEq ι; simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
n : ℕ
hn : HasInjectiveDimensionLE X n
⊢ False

Tactic:
rw [← injectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn

Goal state after:
case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
n : ℕ
hn : ↑n = ⊤
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case refine_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⊤ ≤
    span R
      (range
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))

Tactic:
convert! hw
    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
    rw [ModuleCat.epi_iff_surjective] at hE
    rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),
      Function.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝ : X✝ ⟶ Y✝
⊢ (externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝ ≫
      (NatIso.ofComponents (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom =
    (NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom ≫
      (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝

Tactic:
by ext; simp [whisker_exchange]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C
⊢ (Functor.diag D).Final

Tactic:
apply_rules [final_iff_comp_equivalence _ this.functor |>.mpr,
      final_iff_final_comp e.inverse _ |>.mpr, final_of_natIso sq.symm]

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ (Pi.eval I s).Final

Tactic:
apply Functor.final_of_exists_of_isFiltered

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, Nonempty (d ⟶ (Pi.eval I s).obj c)

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.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₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
rw [← ModuleCat.epi_iff_surjective]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Epi (f.app X)
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 : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''

Tactic:
by
  obtain ⟨U, ⟨x, x', x''⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      ((isColimitOfPreserves (forget AddCommGrpCat) hcM').tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM''))) ⟨m, m', m''⟩
  rw [Prod.ext_iff, Prod.ext_iff] at h
  obtain ⟨rfl, rfl, rfl⟩ := h
  exact ⟨U, x, x', x'', rfl, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
⊢ (R ⋙ F.partialLeftAdjoint).map φ ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g) =
    F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g) ≫ ((const J).obj Y).map φ

Tactic:
by
            apply F.partialLeftAdjointHomEquiv.injective
            have := c.w φ
            dsimp at this ⊢
            rw [comp_id, Equiv.apply_symm_apply, partialLeftAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, reassoc_of% this]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S

Tactic:
let ι' : Type (max u v) := (Presieve.ofArrows X f).uncurry

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S
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
f : Y ⟶ X
S : J.Cover X
I₁ I₂ : (S.pullback f).Arrow
r : I₁.Relation I₂
⊢ r.g₁ ≫ I₁.base.f = r.g₂ ≫ I₂.base.f

Tactic:
simp [r.w_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
J : GrothendieckTopology C
h : IsSheaf J P
⊢ IsSheaf J (P ⋙ uliftFunctor.{w', w})

Tactic:
rwa [isSheaf_comp_uliftFunctor_iff]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
⊢ (bindOfArrows X f fun i ↦ ofArrows (Y i) (g i)) = ofArrows (fun p ↦ Y p.fst p.snd) fun p ↦ g p.fst p.snd ≫ f p.fst

Tactic:
refine le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)
  rintro W u ⟨i, v, ⟨j⟩⟩
  exact ⟨Sigma.mk i j⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i a, g = a ≫ f i) → (ofArrows Y f).arrows g

Tactic:
· rintro ⟨i, a, rfl⟩
    apply downward_closed _ (ofArrows_mk Y f i)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Sieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) = R

Tactic:
ofArrows_category',

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Sieve S
⊢ generate R.arrows = R
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
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.Compatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) ↔
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]
  constructor
  · intro t
    apply SecondObj.ext
    intro Y Z g f hf
    simpa [firstMap, secondMap] using t _ g hf
  · intro t Y Z f g hf
    rw [Types.limit_ext_iff'] at t
    simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩

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.Full
inst✝ : F.Faithful
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h) ≫ F.map g
⊢ S.arrows f

Tactic:
← F.map_comp

Goal state after:
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.Full
inst✝ : F.Faithful
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows 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✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
S : Sieve X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows (F.preimage h ≫ g)

Tactic:
exact S.downward_closed h₁ _

Goal state after: