mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M X X
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀

Tactic:
subst hm₀; simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)

Tactic:
let ψ : mk₃ (0 : R₁.obj' 0 ⟶ _) (R₁.map' 0 1) (R₁.map' 1 2) ⟶
    mk₃ (0 : R₁.obj' 0 ⟶ _) (R₂.map' 0 1) (R₂.map' 1 2) := homMk₃ (𝟙 _) (app' φ 0) (app' φ 1)
      (app' φ 2) (by simp) (naturality' φ 0 1) (naturality' φ 1 2)
  refine mono_of_epi_of_mono_of_mono' ψ (by simp)
    (hR₁.exact 0).exact_toComposableArrows
    (exact₂_mk _ (by simp) ?_) (by dsimp [ψ]; infer_instance) h₀ h₁
  rw [ShortComplex.exact_iff_mono _ (by simp)]
  exact hR₂'

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ 1 • a = a

Tactic:
simp only [smulOfRingMorphism_smul_eq,
        Functor.id_obj, map_one, End.one_def, NatTrans.id_app, id_comp]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ solution.π.ker = relations.map.range

Tactic:
range_map,

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : SpecialLinearGroup n R
⊢ (↑A * ↑B).det = 1

Tactic:
by rw [det_mul, A.prop, B.prop, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
⊢ (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)

Tactic:
by
  ext x
  exact AlgHom.congr_fun (map_comp_map _ _) x

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

Goal state before:
pp: case cons
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
t : TransvectionStruct ι F
L : List (TransvectionStruct ι F)
ih : P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup (t :: L)).prod

Tactic:
| cons t L ih =>

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (B (l (b₁' i))) (r (b₂' j)) = ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
conv_lhs => rw [← LinearMap.sum_repr_mul_repr_mul b₁ b₂]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ((b₁.repr (l (b₁' i))).sum fun i xi ↦ (b₂.repr (r (b₂' j))).sum fun j yj ↦ xi •> yj •> (B (b₁ i)) (b₂ j)) =
    ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x
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
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
B' : BilinMap R M N
h' : ∀ (x y : M), Q' (x + y) = Q' x + Q' y + (B' x) y
x y : M
⊢ (⇑Q + ⇑Q') (x + y) = (⇑Q + ⇑Q') x + (⇑Q + ⇑Q') y + ((B + B') x) y

Tactic:
by
          simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_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✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(if x.1 + x.2 = n then GradedMonoid.GMul.mul (r x.1) (r' x.2) else 0) =
    ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with x.1 + x.2 = n, ↑(r x.1) * ↑(r' x.2)

Tactic:
apply_ite,

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
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      if x.1 + x.2 = n then ↑(GradedMonoid.GMul.mul (r x.1) (r' x.2)) else ↑0) =
    ∑ x ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with x.1 + x.2 = n, ↑(r x.1) * ↑(r' x.2)
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)
r' : ↥(A 0)
j _x : ι
⊢ _x + 0 = j ↔ _x = j

Tactic:
by rw [add_zero]

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

Goal state before:
pp: case add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : involute x = -x
ihy : involute y = -y
⊢ involute (x + y) = -(x + y)

Tactic:
rw [map_add, ihx, ihy, neg_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ ⋃ i_1, ⋃ i_2, ↑((ι Q).range ^ ↑i_1) * ↑((ι Q).range ^ ↑i_2) ⊆ ⋃ i_1, ↑((ι Q).range ^ ↑i_1)

Tactic:
Set.iUnion_subset_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ ∀ (i_1 : { n // ↑n = i }) (i_2 : { n // ↑n = j }),
    ↑((ι Q).range ^ ↑i_1) * ↑((ι Q).range ^ ↑i_2) ⊆ ⋃ i_3, ↑((ι Q).range ^ ↑i_3)
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ Finset.univ ∈ powersetCard (Fin n) n

Tactic:
by rw [mem_iff, Finset.card_univ, Fintype.card_fin]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
⊢ motive x hx

Tactic:
refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx
  obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h
  exact algebraMap r

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

Goal state before:
pp: 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
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v

Tactic:
induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n ih =>
    rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _

Goal state after:
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
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ (toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R = ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R

Tactic:
apply LinearMap.ext

Goal state after:
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ ∀ (x : M),
    ((toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R) x =
      (((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R) x
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HasLimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))

Tactic:
change HasLimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (R.map f).hom)

Goal state after:
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
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HasLimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv

Tactic:
rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
⊢ ∀ (j₁ j₂ : C), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
intro c₁ c₂
        have X : StructuredArrow (c₁, c₂) (diag C) :=
          letI S : Final (diag C) := by infer_instance
          Nonempty.some (S.out (c₁, c₂)).is_nonempty
        use [X.right, c₂]
        constructor
        · constructor
          · exact Zag.of_hom X.hom.fst
          · simpa using Zag.of_inv X.hom.snd
        · rfl

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

Goal state before:
pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
intro _ c _ _
      exact ⟨c, 𝟙 _, rfl⟩

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
⊢ (((colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv) ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J)
              (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
        (HasColimit.isoOfNatIso F.uncurryObjFlip).inv) ≫
      (colimitUncurryIsoColimitCompColim F.flip).hom =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k

Tactic:
simp [Equivalence.counitInv]

Goal state after:
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₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (F₀₁.associator F₁₂ F₂₃).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      (conjugateEquiv (adj₀₂.comp adj₂₃) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (whiskerRight τ₀₁₂ F₂₃)

Tactic:
conjugateEquiv_comp,

Goal state after:
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₀₁.associator F₁₂ F₂₃).hom ≫ (F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      (conjugateEquiv (adj₀₂.comp adj₂₃) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (whiskerRight τ₀₁₂ F₂₃)
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₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (M₂.map φ)) ((ConcreteCategory.hom (f.app X)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)

Tactic:
naturality_apply

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (M₂.map φ)) ((ConcreteCategory.hom (f.app X)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ConcreteCategory.hom (g.app X)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
⊢ R ⊓ S ∈ J X

Tactic:
apply J.transitive rj _ fun Y f Hf => _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsEmpty C
J : GrothendieckTopology C
⊢ J = ⊤

Tactic:
by
  rw [eq_top_iff]
  intro X
  exact IsEmpty.elim ‹IsEmpty C› X

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 : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry →
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
rintro ⟨Y, u, hu⟩; exact ⟨⟨Y, u⟩, hu, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ R h ≤ pullback f (bind S R)

Tactic:
by
  rw [← galoisConnection f]
  apply pushforward_le_bind_of_mem

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ R.arrows f → (functorPushforward (𝟭 C) R).arrows f

Tactic:
· intro hf
    exact ⟨X, f, 𝟙 _, hf, by simp⟩

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Tactic:
intro t ht
    simpa using ht _ (Presieve.singleton_self _)

Goal state after:
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✝
S : Sieve X✝
inst✝¹ : R.HasPairwisePullbacks
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
⊢ F.map f.op ≫ F.map (pullback.fst f f).op = F.map f.op ≫ F.map (pullback.snd f f).op

Tactic:
by simp [← Functor.map_comp, ← op_comp, pullback.condition]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ x₂.IsAmalgamation (e (hP₁.amalgamate x₁ hx₁))

Tactic:
simp only [this, Equiv.symm_apply_apply]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ x₁.IsAmalgamation (hP₁.amalgamate x₁ hx₁)