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
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
let ⟨I', _, f', _⟩ := EnoughInjectives.presentation N

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'
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
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₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
use mk x (⟨a, aS⟩ * s)

Goal state after:
case h
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₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk x (⟨a, aS⟩ * s)) = mk m s
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ ((ιMulti R 1) fun x ↦ m₁ + m₂) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
rw [h]; nth_rw 2 [h]; nth_rw 3 [h]
          simp only [Fin.isValue, AlternatingMap.map_update_add]

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
⊢ P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } } ≫
      (coneOfConeUncurry Q c).π.app j =
    s.π.app j

Tactic:
apply (Q j).hom_ext

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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
⊢ ∀ (j_1 : K),
    (P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } } ≫
          (coneOfConeUncurry Q c).π.app j) ≫
        (D.obj j).π.app j_1 =
      s.π.app j ≫ (D.obj j).π.app j_1
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)
P : IsColimit c
s : Cocone D.coconePoints
j : J
⊢ (coconeOfCoconeUncurry Q c).ι.app j ≫
      P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
apply (Q j).hom_ext

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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        (coconeOfCoconeUncurry Q c).ι.app j ≫
          P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫ s.ι.app j
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✝
⊢ HasPullback (F.map u✝¹) (F.map u✝)

Tactic:
have := Presieve.HasPairwisePullbacks.has_pullbacks hf hg
    have := F.preservesLimit_cospan_of_mem_presieve _ hf hg
    exact hasPullback_of_preservesPullback F _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
⊢ (ConcreteCategory.hom ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) =
    (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂)

Tactic:
simp only [yoneda_obj_obj, Opposite.unop_op, yoneda_obj_map, Quiver.Hom.unop_op]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
⊢ (ConcreteCategory.hom (↾fun g ↦ g₁ ≫ g)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ hf₁) =
    (ConcreteCategory.hom (↾fun g ↦ g₂ ≫ g)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
replace H := Classical.choice H

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
← h f₁ g₁ h₁,

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ x (g₁ ≫ f₁) ⋯ = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
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
f : Y ⟶ X
inst✝ : IsSplitEpi f
⊢ GaloisInsertion (pushforward f) (pullback f)

Tactic:
by
  apply (galoisConnection f).toGaloisInsertion
  intro S Z g hg
  exact ⟨g ≫ section_ f, by simpa⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
y : P.obj (op Y)
⊢ (ConcreteCategory.hom (P.map f.op)) y = x f ⋯ → x.IsAmalgamation y

Tactic:
rintro H Y g ⟨rfl⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y✝ : C
f : X ⟶ Y✝
x : FamilyOfElements P (singleton f)
y : P.obj (op Y✝)
H : (ConcreteCategory.hom (P.map f.op)) y = x f ⋯
Y : C
⊢ (ConcreteCategory.hom (P.map f.op)) y = x f ⋯
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

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

Tactic:
have : ∀ (t₂ : P₂.obj (op X)),
      x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂) := fun t₂ ↦ by
    simp only [FamilyOfElements.IsAmalgamation, x₁,
      ← he', EmbeddingLike.apply_eq_iff_eq]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ ∃! t, x₂.IsAmalgamation t
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
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ ∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })),
    (forkMap R P ≫ firstMap R P) ≫
        limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
      (forkMap R P ≫ secondMap R P) ≫
        limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Tactic:
rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }
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
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : g₁ ≫ (fun i ↦ (Over.map p).map (f i)) i₁ = g₂ ≫ (fun i ↦ (Over.map p).map (f i)) i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
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

Goal state after:
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:
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.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := ⋯
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := ⋯
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op V)⦄,
    (G.sieveOfSection ↑(x i hi)).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
        (ConcreteCategory.hom (F.map f.op)) ↑(x i hi)

Tactic:
intro V'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
⊢ ∀ ⦃f : V' ⟶ unop (op V)⦄,
    (G.sieveOfSection ↑(x i hi)).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
        (ConcreteCategory.hom (F.map f.op)) ↑(x i hi)
Module: Mathlib.CategoryTheory.Sites.Whiskering

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
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
intro X S

Goal state after:
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
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
⊢ ↑(Meq.mk S (mk w)) I = ↑s I

Tactic:
dsimp [Meq.mk]

Goal state after:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
⊢ (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (mk w) = ↑s I
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
have : (Sieve.bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
    rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
    apply hf
  apply Presieve.isSheafFor_subsieve_aux P this
  · apply isSheafFor_bind _ _ _ hR hS
    intro Y f hf Z g
    rw [← Sieve.pullback_comp]
    apply (hS (R.downward_closed hf _)).isSeparatedFor
  · intro Y f hf
    have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => Sieve.pullback k S) =
        R.pullback f := by
      ext Z g
      constructor
      · rintro ⟨W, k, l, hl, _, comm⟩
        rw [pullback_apply, ← comm]
        simp [hl]
      · intro a
        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
        simp [hf]
    rw [this]
    apply hR' hf

Goal state after:
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))

Tactic:
intro X S

Goal state after:
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork E.pt))