mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
let S' : ShortComplex (ModuleCat.{v} R') :=
      ModuleCat.shortComplexOfCompEqZero _ _ f'.hom.exact_map_mkQ_range.linearMap_comp_eq_zero

Goal state after:
case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
suffices ExteriorAlgebra.ιMulti R n (v ∘ α) = 0 by simp [this]
    exact AlternatingMap.map_eq_zero_of_not_injective _ _ <| fun h ↦ α_inj (Injective.of_comp h)

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
← hx,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h)
      (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s)) =
    0
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n) ≫ ι.map p.fst = ι.map p.snd.fst ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)

Tactic:
← ι.map_comp,

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ p.fst) = ι.map p.snd.fst ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ p.fst) = ι.map p.snd.fst ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)

Tactic:
← ι.map_comp,

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ p.fst) = ι.map (p.snd.fst ≫ (Λ.chainComplex Y).d (n + 1) n)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n) ≫ ι.map ((Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1)) ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)

Tactic:
← ι.map_comp,

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1)) ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1)) ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)

Tactic:
← ι.map_comp,

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1) ≫ (Λ.chainComplex Y).d (n + 1) n)
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 : J ⥤ C
j : J
⊢ (λ_ F).inv.app j = (λ_ (F.obj j)).inv

Tactic:
rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_hom_app,
    Iso.inv_hom_id_app]

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
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
| (F.obj j).map f

Tactic:
equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f =>
                      simp

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
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
⊢ ((const J).obj Y).map φ ≫ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j') =
    F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ

Tactic:
by
            apply F.partialRightAdjointHomEquiv.injective
            have := c.w φ
            dsimp at this ⊢
            rw [id_comp, Equiv.apply_symm_apply, partialRightAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, assoc, 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.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ Presieve.pullbackArrows f (Presieve.ofArrows Z g) ∈ J.coverings X

Tactic:
← Presieve.ofArrows_pullback

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ Y
hR : Presieve.ofArrows Z g ∈ J.coverings Y
inst✝ : (Presieve.ofArrows Z g).HasPullbacks f
this : ∀ (i : ι), Limits.HasPullback (g i) f
⊢ (Presieve.ofArrows (fun i ↦ Limits.pullback (g i) f) fun x ↦ Limits.pullback.snd (g x) f) ∈ J.coverings X
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ Over.Hom.left F.hom ≫ x g₂.obj.hom ⋯ = 𝟙 (unop (op g₁.obj.left)) ≫ x g₁.obj.hom ⋯

Tactic:
exact hx _ _ _ _ (by simp)

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
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
⊢ (ofArrows (Y ∘ a) fun i ↦ f (a i)) = ofArrows Y f

Tactic:
refine le_antisymm (ofArrows_comp_le f a) ?_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
⊢ ofArrows Y f ≤ ofArrows (Y ∘ a) fun i ↦ f (a i)
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
⊢ (ofArrows Y f).uncurry = Set.range fun i ↦ ⟨Y i, f i⟩

Tactic:
by
  ext ⟨Z, v⟩; simp only [Set.mem_range, Sigma.mk.injEq]; constructor
  · rintro ⟨i⟩; exact ⟨_, rfl, HEq.refl _⟩
  · rintro ⟨i, rfl, h⟩; rw [← eq_of_heq h]; exact ⟨i⟩

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
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₂
⊢ ∀ (j : Discrete ((Y : C) × { f // R f })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.fst)) j)) z₁ =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.fst)) j)) z₂
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
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j)) z₁ =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.snd.fst)) j)) z₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

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

Tactic:
← ht _,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t =
    (ConcreteCategory.hom (P.map ⋯.choose.op)) ((ConcreteCategory.hom (P.map ⋯.choose.op)) t)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
⊢ (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

Tactic:
apply Limits.Types.limit_ext

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (firstMap P R)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j))
        ((ConcreteCategory.hom (secondMap P R)) x)
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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X✝ : C
S : Sieve X✝
R : Presieve X✝
E : Aᵒᵖ
π : (S.arrows.diagram.op ⋙ P).cones.obj E
X Y : C
f : X ⟶ X✝
g : Y ⟶ X
hf : S.arrows f
⊢ (fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) Y (g ≫ f) ⋯ =
    (ConcreteCategory.hom ((P ⋙ coyoneda.obj E).map g.op))
      ((fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) X f hf)

Tactic:
let φ : S.arrows.categoryMk (g ≫ f) (S.downward_closed hf g) ⟶
        S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ rfl)
      simpa using! π.naturality φ.op

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type t
inst✝ : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type t
inst✝ : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₂
⊢ ∀ (j : Discrete I),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun i ↦ P.obj (op (X i))) j)) z₁ =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun i ↦ P.obj (op (X i))) j)) z₂
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
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

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
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂
⊢ ∀ (j : Discrete (I × I)),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j)) z₁ =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j)) z₂
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
    simpa [firstMap, secondMap] using t

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
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
⊢ ((shrinkFunctor.{w, v₁, u₁} S).toFunctor ⋙ CategoryTheory.uliftFunctor.{w', w}).map f ≫
      (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom =
    (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom ≫
      (shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor.map f

Tactic:
by
      dsimp
      ext
      dsimp [Equiv.subtypeEquiv_apply]
      rw [shrinkYonedaObjObjEquiv_obj_map, shrinkYonedaObjObjEquiv_symm_comp]
      simp

Goal state after:
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
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ ↑(eqv' f₁) = ↑(eqv' f₂)

Tactic:
apply h _ (eqv π).1 <;> exact (eqv' _).2

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

Goal state before:
pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ ∀ (y : (P ⋙ coyoneda.obj (op X)).obj (op Y)),
    (fun t ↦ z.IsAmalgamation t) y → y = ↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯

Tactic:
intro y hy

Goal state after:
case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
⊢ y = ↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
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, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
refine ⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩

Goal state after:
case refine_1.refine_1
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
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t = x i

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) ⋯
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
⊢ Epi p ↔ range p = ⊤

Tactic:
simp [NatTrans.epi_iff_epi_app, epi_iff_surjective, Subfunctor.ext_iff, funext_iff,
    Set.range_eq_univ]

Goal state after: