mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(((decompose 𝒜) 0) 0) = 0

Tactic:
by rw [decompose_zero, zero_apply, ZeroMemClass.coe_zero]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) (x✝¹ + x✝)) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)

Tactic:
rw [decompose_add, add_apply, AddMemClass.coe_add]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n

Tactic:
simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case 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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
⊢ P (x * m)

Tactic:
| mul_mem _i x _hx px m hm =>

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range ^ ↑⟨2, ⋯⟩

Tactic:
rw [Subtype.coe_mk, pow_two]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range * (ι Q).range
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
⊢ Infinite ↑(powersetCard α n)

Tactic:
rw [← not_finite_iff_infinite]
  by_contra finite
  suffices ⋃₀ (SetLike.coe '' powersetCard α n) = Set.univ by
    apply Finite.false (α := α)
    rw [← Set.finite_univ_iff, ← this]
    apply Set.Finite.sUnion (Finite.image SetLike.coe finite)
    aesop
  rw [sUnion_eq_univ_iff]
  intro a
  obtain ⟨s, s_mem, mem_s⟩ := exist_mem_powersetCard_of_inf α n (Nat.pos_of_neZero n) a
  exact ⟨↑s, mem_image_of_mem SetLike.coe s_mem, mem_coe.mpr mem_s⟩

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x : ↑(M F)
⊢ 0 • x = 0

Tactic:
by
    obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
    simp [← colimit_zero_eq]

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 m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
⊢ HasInjectiveDimensionLT X m

Tactic:
by
  let := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  exact e.eq_zero_of_hasInjectiveDimensionLT n (by lia)

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
⊢ (presentation R n M).postcomp f = (presentation R n M).postcomp g

Tactic:
by ext f; apply DFunLike.congr_fun heq

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
⊢ ∃ l, List.IsChain Zag (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = c₂

Tactic:
have X : StructuredArrow (c₁, c₂) (diag C) :=
          letI S : Final (diag C) := by infer_instance
          Nonempty.some (S.out (c₁, c₂)).is_nonempty

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ ∃ l, List.IsChain Zag (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = c₂
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
X : C₀
hX : P X
Y : C₀
hY : P Y
⊢ ∃ Z x x, True

Tactic:
obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
X : C₀
hX : P X
Y : C₀
hY : P Y
Z : C₀
hZ : P Z
f : IsFiltered.max X Y ⟶ Z
⊢ ∃ Z x x, True
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
have : IsFiltered P.FullSubcategory :=
      { nonempty := by
          obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
          exact ⟨X, hX⟩
        cocone_objs := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩
          obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩
        cocone_maps := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩ }

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this : IsFiltered P.FullSubcategory
⊢ ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
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
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    s.π.app (j, k).1 ≫ (D.obj (j, k).1).π.app (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2

Tactic:
rcases p' with ⟨j', k'⟩

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
k : K
j' : J
k' : K
f : (j, k) ⟶ (j', k')
⊢ s.π.app (j', k').1 ≫ (D.obj (j', k').1).π.app (j', k').2 =
    s.π.app (j, k).1 ≫ (D.obj (j, k).1).π.app (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj (j', k').1).map f.2
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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ (Pi.eval I s).Initial

Tactic:
apply Functor.initial_of_exists_of_isCofiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c' ⟶ c s)) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨eq f g, eqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using eq_condition _ _

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)
P : IsColimit c
s : Cocone D.coconePoints
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2 ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    (D.obj (j, k).1).ι.app (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt

Tactic:
rcases p' with ⟨j', k'⟩

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
k : K
j' : J
k' : K
f : (j, k) ⟶ (j', k')
⊢ (F.map f.1).app (j, k).2 ≫ (F.obj (j', k').1).map f.2 ≫ (D.obj (j', k').1).ι.app (j', k').2 ≫ s.ι.app (j', k').1 =
    (D.obj (j, k).1).ι.app (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt
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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
Q' : (j : J) → IsLimit (Q.obj j) := fun j ↦ limit.isLimit ((curry.obj G).obj j)
c' : Cone G
f : J × K
⊢ limit.lift (curry.obj G ⋙ lim) (coneOfConeCurry G Q' c') ≫ (coneOfHasLimitCurryCompLim G).π.app f = c'.π.app f

Tactic:
simp [coneOfHasLimitCurryCompLim, Q, Q']

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 : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap (R.map φ) ≫ c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv (((R ⋙ F.partialLeftAdjoint).map φ ≫ c'.ι.app j') ≫ f)

Tactic:
assoc

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap (R.map φ) ≫ c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv ((R ⋙ F.partialLeftAdjoint).map φ ≫ c'.ι.app j' ≫ 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 : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = eqToHom ⋯ ≫ f
⊢ map F R f

Tactic:
eqToHom_refl,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = 𝟙 (F.obj Z) ≫ f
⊢ map F R f
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
i : I
h : W ⟶ Y i
⊢ ∃ i a, g = a ≫ f i

Tactic:
exact ⟨i, h, hX.hom_ext _ _⟩

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
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ X},
    (∃ t, (hom (f.app (Opposite.op Y))) t = f_1) → ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = g ≫ f_1

Tactic:
by
    rintro Y Z _ ⟨t, rfl⟩ g
    refine ⟨R.map g.op t, ?_⟩
    simp

Goal state after:
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₂ : P₂.obj (op X)
⊢ x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)

Tactic:
by
    simp only [FamilyOfElements.IsAmalgamation, x₁,
      ← he', EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: 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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom
        ((J.diagramPullback P f).app (op S) ≫
          colimit.ι ((J.pullback f).op ⋙ J.diagram P Y) (op S) ≫ colimit.pre (J.diagram P Y) (J.pullback f).op))
      ((Meq.equiv P S).symm x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))

Tactic:
colimit.ι_pre,

Goal state after:
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((J.diagramPullback P f).app (op S) ≫ colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))))
      ((Meq.equiv P S).symm x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: 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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom
        ((J.diagramPullback P I.f).app (op S) ≫
          colimit.ι ((J.pullback I.f).op ⋙ J.diagram P I.Y) (op S) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f).op))
      ((Meq.equiv P S).symm x)

Tactic:
colimit.ι_pre,

Goal state after:
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom
        ((J.diagramPullback P I.f).app (op S) ≫ colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))))
      ((Meq.equiv P S).symm x)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      ⊤.toMultiequalizer P ≫
        (J.diagram P I.Y).map ee.op ≫
          colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))) =
    (J.diagramPullback P (Cover.Arrow.map I e.op.unop).f.op.unop).app S ≫
      colimit.ι
          ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op ⋙
            J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
          S ≫
        colimit.pre (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
          (J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op

Tactic:
colimit.ι_pre,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      ⊤.toMultiequalizer P ≫
        (J.diagram P I.Y).map ee.op ≫
          colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))) =
    (J.diagramPullback P (Cover.Arrow.map I e.op.unop).f.op.unop).app S ≫
      colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)
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 : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

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

Goal state after:
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 : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this :
  (ConcreteCategory.hom (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) ⋯).op)) (↑s i₁) =
    (ConcreteCategory.hom (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) ⋯).op)) (↑s i₂)
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((sheafify J G).toFunctor.map f_1 ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
      (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map f_1

Tactic:
intro U V i
    ext s
    apply (h _ ((Subfunctor.sheafify J G).toFunctor.map i s).prop).isSeparatedFor.ext
    intro W j hj
    refine (Presieve.IsSheafFor.valid_glue (h _ ((G.sheafify J).toFunctor.map i s).2)
      ((G.family_of_elements_compatible _).map _) _ hj).trans ?_
    dsimp
    simp only [← comp_apply, ← Functor.map_comp]
    change _ = F'.map (j ≫ i.unop).op _
    refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
    · simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]
      rfl
    · dsimp [Presieve.FamilyOfElements.map] at hj ⊢
      rwa [Functor.map_comp, comp_apply]

Goal state after: