mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (∑ i, w i • v i)

Tactic:
rw [← v.equivFun_symm_apply]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (v.equivFun.symm w)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
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
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * y * b) ⋯

Tactic:
mul_assoc _ y b

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
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
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * (y * b)) ⋯
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) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt

Tactic:
apply hom_ext
  apply LinearMap.ext
  simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
    AlgHom.toLinearMap_apply, map_apply_ι, toTrivSqZeroExt_ι, TrivSqZeroExt.map_inr, forall_const]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
⊢ injectiveDimension X < ↑n ↔ HasInjectiveDimensionLT X n

Tactic:
exact injectiveDimension_lt_iff

Goal state after:
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 : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
      𝟙 (limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X))))) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom

Tactic:
comp_id

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 : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom
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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      𝟙 (limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))) =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom

Tactic:
comp_id

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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom
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✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition (F.map f) (F.map g))]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩

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)

pp: case refine_2
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 : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
· intro d
    obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
    exact ⟨_, ⟨f.hom⟩⟩

Goal state after:
case refine_2
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 : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

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

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝

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

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝
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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (Prod.mkHom (𝟙 j) (𝟙 k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
← prod_id,

Goal state after:
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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (𝟙 (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
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.partialRightAdjointHomEquiv (f ≫ 𝟙 (F.partialRightAdjointObj Y)) ≫ g.hom = F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
comp_id

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.partialRightAdjointHomEquiv f ≫ g.hom = F.partialRightAdjointHomEquiv f ≫ g.hom
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 : F.obj X ⟶ Y.obj
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv.symm f ≫ F.partialRightAdjointMap g = F.partialRightAdjointHomEquiv.symm (f ≫ g.hom)

Tactic:
by
  simp [Equiv.eq_symm_apply, partialRightAdjointHomEquiv_map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ f i = eqToHom ⋯ ≫ f i

Tactic:
simp only [eqToHom_refl, id_comp]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

Tactic:
· intro H
    refine Nonempty.intro ?_
    exact
    { desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
        (yonedaFamily_fromCocone_compatible S s) |>.choose
      fac := by
        intro s f
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        have ht := H.choose_spec.1 f.obj.hom f.property
        cat_disch
      uniq := by
        intro s Fs HFs
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        apply H.choose_spec.2 Fs
        exact fun _ f hf => HFs ⟨Over.mk f, hf⟩ }

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f

Tactic:
· rw [id_comp]
    exact h.choose_spec.choose_spec.2

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofObjects Y X).arrows g → (ofArrows Y f).arrows g

Tactic:
rw [mem_ofArrows_iff, mem_ofObjects_iff]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1

Tactic:
intro W a

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R f → Presieve.functorPushforward F (generate R).arrows f

Tactic:
· rintro ⟨X', g, f', h₁, h₂⟩
    exact ⟨X', g, f', le_generate R _ _ h₁, h₂⟩

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✝
hf : R.arrows f
⊢ (functorPushforward (𝟭 C) R).arrows f

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

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x j)

Tactic:
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
i j : I
t :
  (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j)))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j)))
      ((ConcreteCategory.hom (secondMap P X π)) x)
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x j)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t) →
    ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))

Tactic:
rintro h ⟨E, π⟩
    let eqv := conesEquivSieveCompatibleFamily P S (op E)
    rw [← eqv.left_inv π]
    erw [(homEquivAmalgamation (eqv π).2).uniqueCongr.nonempty_congr]
    rw [unique_subtype_iff_existsUnique]
    exact h _ _ (eqv π).2

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

Goal state before:
pp: case refine_2
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
x : FirstObj P X
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) j)

Tactic:
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t

Goal state after:
case refine_2
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
x : FirstObj P X
i j : I
t :
  (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j)))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j)))
      ((ConcreteCategory.hom (secondMap P X π)) x)
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x) j)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ ≤ pullback g (ofArrows X f)

Tactic:
Sieve.ofArrows,

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ generate (Presieve.ofArrows P p₁) ≤ pullback g (ofArrows X f)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf J A
X : Cᵒᵖ
⊢ ⊥ ∈ J (unop X)

Tactic:
simp [H]

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

Goal state before:
pp: case refine_1.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t ↦ hx.familyOfElements.IsAmalgamation t) y → y = t
t' : (fun X ↦ X) (P.obj (op B))
ht' : (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) t'
x✝² : C
x✝¹ : x✝² ⟶ B
x✝ : ofArrows X π x✝¹
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t' = hx.familyOfElements (π i) ⋯

Tactic:
· rw [ht', hx.familyOfElements_ofArrows_mk]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
e : P.obj (op X) ≅ multiequalizer (S.index P) := h.conePointUniqueUpToIso (limit.isLimit (S.index P).multicospan)
⊢ IsIso (S.toMultiequalizer P)

Tactic:
exact (inferInstance : IsIso e.hom)

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

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : (sheafificationAdjunction J D).unit.app P ≫ γ = η
γ' : (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ } := { hom := γ }
⊢ γ = (((sheafificationAdjunction J D).homEquiv P { obj := Q, property := hQ }).symm η).hom

Tactic:
change γ'.hom = _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : (sheafificationAdjunction J D).unit.app P ≫ γ = η
γ' : (presheafToSheaf J D).obj P ⟶ { obj := Q, property := hQ } := { hom := γ }
⊢ γ'.hom = (((sheafificationAdjunction J D).homEquiv P { obj := Q, property := hQ }).symm η).hom
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ ((sheafifyCocone E).ι.app k).hom = E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [← cancel_epi ((sheafToPresheaf _ _).map
    ((sheafificationAdjunction J D).counit.app (F.obj k)))]
  dsimp [sheafifyCocone]
  rw [← ObjectProperty.FullSubcategory.comp_hom_assoc,
    ← NatTrans.comp_app, IsIso.hom_inv_id, NatTrans.id_app]
  dsimp
  rw [Category.id_comp, toSheafify_naturality, sheafificationAdjunction_counit_app_val,
    sheafifyLift_id_toSheafify_assoc]

Goal state after: