mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ homEquiv e ≫ ((singleFunctors C).shiftIso (↑n + 1) (-(↑n + 1)) 0 ⋯).hom.app Y = 0

Tactic:
apply from_singleFunctor_obj_eq_zero_of_projective
    (L := (CochainComplex.singleFunctor C (-(n + 1))).obj Y) (n := -(n + 1)) _ (by lia)

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
k l : ℕ
M : Type u_7
inst✝ : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n M)
⊢ toUnits ↑ζ ∈ rootsOfUnity n Mˣ

Tactic:
by
    simp only [mem_rootsOfUnity, ← map_pow, EmbeddingLike.map_eq_one_iff]
    exact (mem_rootsOfUnity ..).mp ζ.prop

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
g : GL n R
⊢ (map f) g * (map f) g⁻¹ = 1

Tactic:
by
  simp only [map_inv, mul_inv_cancel]

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

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
simp [smul_mulVec, mul_eq_zero_iff_left h]

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

Tactic:
simpa [← hr, Submonoid.smul_def, Units.smul_def] using! smul_one_eq_diagonal r

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

Goal state before:
pp: case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) ({i | i ≠ i₀}.prod g)

Tactic:
rw [diag_decompose i₀ D hD]

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
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ ((map g).comp (map f)) x = x

Tactic:
map_comp_map,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map (g.comp f)) x = x
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
s : R
x y : GradedMonoid A
⊢ (s • x) • y = s • x • y

Tactic:
by
    dsimp
    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]

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✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)

Tactic:
intro ai

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
⊢ ∀ (y : A ai), (mulHom A) ((of A ai) y) = (mulHom A).flip ((of A ai) y)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ (P * A₁ * P⁻¹)ᵀ * J = J * (P * A₂ * P⁻¹)

Tactic:
simp only [Matrix.transpose_mul]

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ P⁻¹ᵀ * (A₁ᵀ * Pᵀ) * J = J * (P * A₂ * P⁻¹)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Tactic:
by
  rw [skewAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule]
  simp [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]

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

Goal state before:
pp: R : Type u_3
N : Type u_5
P : Type u_6
n : Type w
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing R
inst✝⁴ : Invertible 2
inst✝³ : AddCommGroup N
inst✝² : Module R N
b : Basis n R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
b' : Basis n R P
Q : QuadraticForm R P
f : N →ₗ[R] P
⊢ discr b (QuadraticMap.comp Q f) = ((LinearMap.toMatrix b b') f).det * ((LinearMap.toMatrix b b') f).det * discr b' Q

Tactic:
by
  simp [mul_left_comm, toMatrix_comp b b', mul_comm, discr]

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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ motive x hx

Tactic:
apply Submodule.iSup_induction' (motive := motive) _ _ (range_ι_pow 0 (Submodule.zero_mem _)) add
  refine Subtype.rec ?_
  simp_rw [ZMod.natCast_eq_iff, add_comm n.val]
  rintro n' ⟨k, rfl⟩ xv
  simp_rw [pow_add, pow_mul]
  intro hxv
  induction hxv using Submodule.mul_induction_on' with
  | mem_mul_mem a ha b hb =>
    induction ha using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      simp_rw [← Algebra.smul_def]
      exact range_ι_pow _ (Submodule.smul_mem _ _ hb)
    | add x y n hx hy ihx ihy =>
      simp_rw [add_mul]
      apply add _ _ _ _ ihx ihy
    | mem_mul x hx n'' y hy ihy =>
      revert hx
      simp_rw [pow_two]
      intro hx2
      induction hx2 using Submodule.mul_induction_on' with
      | mem_mul_mem m hm n hn =>
        simp_rw [LinearMap.mem_range] at hm hn
        obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
        simp_rw [mul_assoc _ y b]
        exact ι_mul_ι_mul _ _ _ _ ihy
      | add x hx y hy ihx ihy =>
        simp_rw [add_mul]
        apply add _ _ _ _ ihx ihy
  | add x y hx hy ihx ihy =>
    apply add _ _ _ _ ihx ihy

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ x₂.comp (Ext.mk₀ S.g) ⋯ = 0

Tactic:
x₂.eq_zero_of_hasInjectiveDimensionLT n (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ Ext.comp 0 (Ext.mk₀ S.g) ⋯ = 0
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE (of R (ULift.{v', v} ↑M)) n ↔ HasInjectiveDimensionLE N n

Tactic:
← hasInjectiveDimensionLE_iff_of_linearEquiv_aux (e.symm.trans eM)

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE N n ↔ HasInjectiveDimensionLE N n
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
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ IsFiltered (CostructuredArrow F d)ᵒᵖ

Tactic:
suffices IsFiltered (StructuredArrow (op d) F.op) from
    IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ IsFiltered (StructuredArrow (op d) F.op)
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:
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.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd

Tactic:
apply freeYonedaEquiv_symm_app

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 : C ⥤ D
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.map f ≫ F.partialRightAdjointHomEquiv (𝟙 (F.partialRightAdjointObj Y)) ≫ g.hom =
    F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
← assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ (F.map f ≫ F.partialRightAdjointHomEquiv (𝟙 (F.partialRightAdjointObj Y))) ≫ g.hom =
    F.partialRightAdjointHomEquiv f ≫ g.hom
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
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g)) =
    ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
      ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g)

Tactic:
by ext : 1; exact (ModuleColimit.comp_map ..).symm

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₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)) (m : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (a • n) =
      a • (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n

Tactic:
intro a m₁ m₂; dsimp; erw [M₂.map_smul, TensorProduct.tmul_smul (r := R.map f a)]; 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₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ ∀ (m : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (𝟙 X))) (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n) =
      (ModuleCat.Hom.hom
          ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 X))) ⋯).inv.app
            (M₁.obj X ⊗ M₂.obj X)))
        (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n)

Tactic:
by
    intro m₁ m₂
    dsimp [tensorObjMap]
    simp
    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
x✝³ x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom).app X✝ =
    ((α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom).app X✝

Tactic:
apply pentagon

Goal state after:
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
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ J Y

Tactic:
simp [sj]

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
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))

Tactic:
Types.type_equalizer_iff_unique,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (y : FirstObj P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) y = (ConcreteCategory.hom (secondMap P S)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = y
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R

Tactic:
ext X f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f ↔ R.arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

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

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
    obtain ⟨X, g, h, hg, rfl⟩ := hf
    exact R.downward_closed hg h

Goal state after:
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
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔ Nonempty (IsLimit (Fork.ofι (forkMap P R) ⋯))

Tactic:
Types.type_equalizer_iff_unique,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (y : FirstObj P R),
      (ConcreteCategory.hom (firstMap P R)) y = (ConcreteCategory.hom (secondMap P R)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = y
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ IsSheafFor P (Presieve.ofArrows X π) ↔ Nonempty (IsLimit (Fork.ofι (forkMap P X π) ⋯))

Tactic:
Types.type_equalizer_iff_unique,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ IsSheafFor P (Presieve.ofArrows X π) ↔
    ∀ (y : FirstObj P X),
      (ConcreteCategory.hom (firstMap P X π)) y = (ConcreteCategory.hom (secondMap P X π)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P X π)) x = y
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
Types.type_equalizer_iff_unique,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.right b)

Tactic:
rw [← E.w (WalkingMulticospan.Hom.fst b),
        ← (S.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]

Goal state after:
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ (hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b))) ≫
      (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor P (ofArrows (fun i ↦ (Over.map p).obj (Y i)) fun i ↦ (Over.map p).map (f i))

Tactic:
by
  let e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
      Subtype (Arrows.Compatible P (fun i ↦ (Over.map p).map (f i))) :=
    { toFun s := ⟨fun i ↦ s.val i, fun i₁ i₂ Z g₁ g₂ h ↦ by
        replace h := (Over.forget _).congr_map h
        dsimp at h
        have := s.property i₁ i₂ (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom))
          (Over.homMk g₁.left) (Over.homMk g₂.left (by
            have := Over.w (f i₂)
            dsimp at this ⊢
            rw [reassoc_of% h, this])) (by cat_disch)
        let φ : Z ⟶ (Over.map p).obj (Over.mk (g₁.left ≫ (f i₁).left ≫ X.hom)) :=
          Over.homMk (𝟙 _) (by simpa using Over.w g₁)
        replace this := congr_arg (P.map φ.op) this
        dsimp at this
        simp only [← comp_apply, ← Functor.map_comp, ← op_comp] at this
        convert! this <;> cat_disch⟩
      invFun s := ⟨fun i ↦ s.val i, fun i₁ i₂ Z g₁ g₂ h ↦
        s.property i₁ i₂ _ ((Over.map p).map g₁) ((Over.map p).map g₂)
          (by simp only [← Functor.map_comp, h])⟩ }
  simp only [isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← e.bijective.of_comp_iff']
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst✝ : s.ReflectsIsomorphisms
this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := reflectsLimits_of_reflectsIsomorphisms
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
exact ⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.sheafification D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ≅ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.sheafification E

Tactic:
by
  refine associator _ _ _ ≪≫ ?_
  refine isoWhiskerLeft (J.plusFunctor D) (J.plusFunctorWhiskerRightIso _) ≪≫ ?_
  refine ?_ ≪≫ associator _ _ _
  refine (associator _ _ _).symm ≪≫ ?_
  exact isoWhiskerRight (J.plusFunctorWhiskerRightIso _) (J.plusFunctor E)

Goal state after: