mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
⊢ ∃ c, y + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)

Tactic:
refine ⟨-B x y / B x x, fun z hz => ?_⟩

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y z : V
hz : z ∈ K ∙ x
⊢ (B z) (y + (-(B x) y / (B x) x) • x) = 0
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ ↑(ofFinEmb n β f) = range ⇑f

Tactic:
ext
  simp [mem_ofFinEmb_iff_mem_range]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case e_6
R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
x✝ : (i : ι ⊕ ι') → N i
⊢ (fun t ↦ Sum.rec (fun i ↦ x✝ (Sum.inl i)) (fun i' ↦ x✝ (Sum.inr i')) t) = x✝

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑(n + 1)

Tactic:
exact ⟨n, fun i hi ↦ hasInjectiveDimensionLT_of_ge _ (n + 1) _ (by simpa using hi),
        by simp [ENat.WithBot.lt_add_one_iff]⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Epi p
⊢ ∃ f', f' ≫ p = f

Tactic:
rw [epi_iff_surjective] at hp

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
⊢ ∃ f', f' ≫ p = f
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
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    (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) ≫
      limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j

Tactic:
simp only [Functor.map_comp, assoc, ← Functor.assoc, preservesLimitIso_hom_π,
      ← ModuleCat.restrictScalarsComp'App_inv_naturality]

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
j : J
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j =
    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))) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
              (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j)).inv
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case refine_2
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ h₂.homEquiv ((f ≫ g) ≫ snd X Y) = (ConcreteCategory.hom (G.map f.op)) (h₂.homEquiv (g ≫ snd X Y))

Tactic:
simp [h₂.homEquiv_comp]

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✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
k : K
j : J
⊢ (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
simp [limitFlipCompLimIsoLimitCompLim]

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₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : 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₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ e₀₂₃.symm.hom ≫ G₃₂.whiskerLeft e₀₁₂.symm.hom =
    e₀₁₃.symm.hom ≫ whiskerRight e₁₂₃.symm.hom G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
by simpa using congr_arg Iso.inv h

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₃✝ Y₁✝ Y₂✝ Y₃✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
⊢ ((x✝² ⊗ₘ x✝¹) ⊗ₘ x✝) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom = (α_ X₁✝ X₂✝ X₃✝).hom ≫ (x✝² ⊗ₘ x✝¹ ⊗ₘ x✝)

Tactic:
by ext1; apply associator_naturality

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C ≤ ⊤

Tactic:
exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)

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

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

Tactic:
rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]

Goal state after:
case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.fst g f ≫ g ≫ inv g = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
X : C
R : Presieve X
inst✝¹ : F.PreservesPairwisePullbacks R
inst✝ : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
x✝¹ : map F R f
g : Z ⟶ F.obj X
x✝ : map F R g
Y✝¹ : C
u✝¹ : Y✝¹ ⟶ X
hf : R u✝¹
Y✝ : C
u✝ : Y✝ ⟶ X
hg : R u✝
this : HasPullback u✝¹ u✝
⊢ HasPullback (F.map u✝¹) (F.map u✝)

Tactic:
have := F.preservesLimit_cospan_of_mem_presieve _ hf hg

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
X : C
R : Presieve X
inst✝¹ : F.PreservesPairwisePullbacks R
inst✝ : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
x✝¹ : map F R f
g : Z ⟶ F.obj X
x✝ : map F R g
Y✝¹ : C
u✝¹ : Y✝¹ ⟶ X
hf : R u✝¹
Y✝ : C
u✝ : Y✝ ⟶ X
hg : R u✝
this✝ : HasPullback u✝¹ u✝
this : PreservesLimit (cospan u✝¹ u✝) F
⊢ HasPullback (F.map u✝¹) (F.map u✝)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti

Tactic:
· rintro T u ⟨ij⟩
        use Z ij.1, p (g ij.1) ⟨ij.1⟩ ij.2, g ij.1, ⟨ij.1⟩
        rw [hp]
        exact ⟨⟨_⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
m : s.pt ⟶ (Fork.ofι f w).pt
⊢ m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
hm

Goal state after:
case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
m : s.pt ⟶ (Fork.ofι f w).pt
hm : m ≫ (Fork.ofι f w).ι = s.ι
⊢ m = ↾fun i ↦ Classical.choose ⋯
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
hF : (X : C) → IsTerminal (F.obj X)
⊢ IsTerminal F

Tactic:
refine evaluationJointlyReflectsLimits _
    fun X ↦ IsLimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
hF : (X : C) → IsTerminal (F.obj X)
X : C
⊢ (Cone.postcompose ((empty D).emptyExt (empty (C ⥤ D) ⋙ (evaluation C D).obj X)).hom).obj (asEmptyCone (F.obj X)) ≅
    ((evaluation C D).obj X).mapCone (asEmptyCone F)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h₁ : S.arrows f✝
h₂ : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∧ R.arrows (g ≫ f✝)

Tactic:
simp [h₁, h₂]

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

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

Tactic:
rintro ⟨_, _, _, hu, rfl⟩

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
X : C
s : Presieve X
Z : D
w✝² : C
w✝¹ : w✝² ⟶ X
w✝ : Z ⟶ F.obj w✝²
hu : s w✝¹
⊢ (generate (Presieve.map F s)).arrows (w✝ ≫ F.map w✝¹)
Module: Mathlib.CategoryTheory.Sites.Sieves

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

Tactic:
· rintro ⟨_, _, _, hu, rfl⟩; exact ⟨_, _, _, ⟨hu⟩, 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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : { x // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
⊢ (unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).map g ≫ ↑x (unop f').obj.hom ⋯ =
    ↑x (unop f).obj.hom ⋯ ≫ (S.arrows.diagram.op ⋙ P).map g

Tactic:
have := x.2 f.unop.1.hom g.unop.hom.left f.unop.2

Goal state after:
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ᵒᵖ
x : { x // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  ↑x (Over.Hom.left g.unop.hom ≫ (unop f).obj.hom) ⋯ =
    (ConcreteCategory.hom ((P ⋙ coyoneda.obj E).map (Over.Hom.left g.unop.hom).op)) (↑x (unop f).obj.hom ⋯)
⊢ (unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).map g ≫ ↑x (unop f').obj.hom ⋯ =
    ↑x (unop f).obj.hom ⋯ ≫ (S.arrows.diagram.op ⋙ P).map g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
Y : Cᵒᵖ
u : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hu : u ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ (ConcreteCategory.hom (((shrinkFunctor.{w, v₁, u₁} S).ι ≫ g).app Y)).toFun ⟨u, hu⟩ =
    (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv u).op)) (shrinkYonedaEquiv g)

Tactic:
rw [shrinkYonedaEquiv_naturality, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_shrinkYoneda_map]

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
Y : Cᵒᵖ
u : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hu : u ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ (ConcreteCategory.hom (((shrinkFunctor.{w, v₁, u₁} S).ι ≫ g).app Y)).toFun ⟨u, hu⟩ =
    (ConcreteCategory.hom (g.app (op (unop Y)))) (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv u))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a✝),
      (ConcreteCategory.hom
            (((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫
                  (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
              a✝))
          x =
        (ConcreteCategory.hom ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝)) x) ↔
    (S.functorInclusion ≫ b).app a✝ = a.app a✝

Tactic:
ConcreteCategory.hom_ext_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a✝),
      (ConcreteCategory.hom
            (((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫
                  (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
              a✝))
          x =
        (ConcreteCategory.hom ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝)) x) ↔
    ∀ (x : S.functor.obj a✝),
      (ConcreteCategory.hom ((S.functorInclusion ≫ b).app a✝)) x = (ConcreteCategory.hom (a.app a✝)) x
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
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      (ConcreteCategory.hom (firstMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) =
          (ConcreteCategory.hom (secondMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            ((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a

Tactic:
simp_rw [← compatible_iff_of_small, ← Iso.toEquiv_apply, Equiv.trans_apply,
    Equiv.apply_symm_apply, Equiv.symm_apply_apply]

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
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      Arrows.Compatible P π a →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm
              ((equivShrink ((j : I) → P.obj (op (X j)))) a)
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₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
        (x.Compatible → ∃ t, x.IsAmalgamation t)) ↔
    IsSheafFor P R

Tactic:
apply forall_congr'

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ ∀ (a : FamilyOfElements P R),
    (∀ (t₁ t₂ : P.obj (op X)), a.IsAmalgamation t₁ → a.IsAmalgamation t₂ → t₁ = t₂) ∧
        (a.Compatible → ∃ t, a.IsAmalgamation t) ↔
      a.Compatible → ∃! t, a.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
this : PreservesLimitsOfSize.{0, 0, max u₁ v₁, max u₁ v₁, u₂, (max u₁ v₁) + 1} (coyoneda.obj (op U)) := ⋯
⊢ IsLimit (Fork.ofι (forkMap S.arrows P') ⋯)

Tactic:
apply Classical.choice (h _ S.arrows _)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
this : PreservesLimitsOfSize.{0, 0, max u₁ v₁, max u₁ v₁, u₂, (max u₁ v₁) + 1} (coyoneda.obj (op U)) := ⋯
⊢ generate S.arrows ∈ J X
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
⊢ (Sieve.pullback (l ≫ h) (B hf)).arrows m →
    (ConcreteCategory.hom (P.map m.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) =
      (ConcreteCategory.hom (P.map m.op))
        ((ConcreteCategory.hom (P.map l.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf)))

Tactic:
hm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
⊢ (ConcreteCategory.hom (P.map m.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) =
    (ConcreteCategory.hom (P.map m.op))
      ((ConcreteCategory.hom (P.map l.op)) ((ConcreteCategory.hom (P.map h.op)) (t f hf)))