mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * ↑r' else 0) = ↑(r j) * ↑r'

Tactic:
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r then ↑(r j) * ↑r' else 0) = ↑(r j) * ↑r'
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then 0 * ↑rj else 0) = 0

Tactic:
zero_mul,

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then 0 else 0) = 0
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ this.toFinset ∈ powersetCard α n

Tactic:
rwa [mem_iff, ← ENat.natCast_inj, ← this.encard_eq_coe_toFinset_card]

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Infinite α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
have : NeZero n := NeZero.of_pos h1
    infer_instance

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
x : (n : ℕ) × ↑(powersetCard α n)
⊢ (fun x ↦ ⟨#x, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) x) = x

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]
  exact one_ne_zero ∘ And.right

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯)
          (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m)))
        x 0) =
    AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i ↦ (f (i + 1)).curryLeft m) x
        0)

Tactic:
foldl_ι

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯)
          (((LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f))
        x 0) =
    AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i ↦ (f (i + 1)).curryLeft m) x
        0)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ 𝟙 X = 0

Tactic:
apply Ext.homEquiv₀.symm.injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
this : HasExt C := ⋯
⊢ Ext.homEquiv₀.symm (𝟙 X) = Ext.homEquiv₀.symm 0
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
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext Y X i
⊢ n ≤ i

Tactic:
lia

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

Tactic:
lia

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

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
⊢ n ≤ i

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext Y S.X₃ i
⊢ n + 1 ≤ 1 + i

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ n ≤ i

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext Y X i
⊢ e = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi
      exact this e k rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
⊢ n + k + 1 = d

Tactic:
lia

Goal state after:
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 : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
this : Nonempty (StructuredArrow (c₁, c₂) (Functor.diag C))
⊢ ∀ (j₁ j₂ : StructuredArrow (c₁, c₂) (Functor.diag C)), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
rintro ⟨_, c, f⟩ ⟨_, c', g⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
this : Nonempty (StructuredArrow (c₁, c₂) (Functor.diag C))
left✝¹ : Discrete PUnit.{1}
c : C
f : (fromPUnit (c₁, c₂)).obj left✝¹ ⟶ (Functor.diag C).obj c
left✝ : Discrete PUnit.{1}
c' : C
g : (fromPUnit (c₁, c₂)).obj left✝ ⟶ (Functor.diag C).obj c'
⊢ ∃ l,
    List.IsChain Zag ({ left := left✝¹, right := c, hom := f } :: l) ∧
      ({ left := left✝¹, right := c, hom := f } :: l).getLast ⋯ = { left := left✝, right := c', hom := g }
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
this : IsIso (𝟙 T)
⊢ (map₂ f (𝟙 T)).Final

Tactic:
apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)

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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (Prod.mkHom (f₁, f₂).1 (𝟙 x.2) ≫ Prod.mkHom (𝟙 y.1) (f₁, f₂).2) ≫
      colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ (curry.obj G ⋙ colim).map f₁ ≫ colimit.ι (curry.obj G ⋙ colim) y.1

Tactic:
G.map_comp_assoc,

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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (Prod.mkHom (f₁, f₂).1 (𝟙 x.2)) ≫
      G.map (Prod.mkHom (𝟙 y.1) (f₁, f₂).2) ≫
        colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ (curry.obj G ⋙ colim).map f₁ ≫ colimit.ι (curry.obj G ⋙ colim) y.1
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
⊢ M.map (F.op.map (𝟙 X)) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
      (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))

Tactic:
by
      refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
      exact (M.congr_map_apply (F.op.map_id X) x).trans (by simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
⊢ comap (𝟭 C) K = K

Tactic:
ext
  simp

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry → ⟨Z, v⟩ ∈ {⟨Y, u⟩}

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ {⟨Y, u⟩} → ⟨Z, v⟩ ∈ (singleton u).uncurry

Tactic:
· rintro ⟨⟩; rfl

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ {⟨Y, u⟩} → ⟨Z, v⟩ ∈ (singleton u).uncurry
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)
⊢ x.Compatible ↔
    ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)

Tactic:
refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩

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)
H :
  ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
    p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
⊢ ∀ (h₁ : singleton f f₁) (h₂ : singleton f f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
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
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) →
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x →
    Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)

Tactic:
· intro t
    apply SecondObj.ext
    intro Y Z g f hf
    simpa [firstMap, secondMap] using t _ g hf

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x →
    Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
⊢ ofObjects Y X = ⊤

Tactic:
ext Z h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ (ofObjects Y X).arrows h ↔ ⊤.arrows 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 : C
f : X ⟶ Y
S : Sieve (F.obj Y)
⊢ functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

Tactic:
ext
  simp

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 : C
f : Y ⟶ X
S : Sieve X
⊢ S ≤ functorPullback F (functorPushforward F S)

Tactic:
exact Sieve.le_functorPushforward_pullback _ _

Goal state after:
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 w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
Arrows.pullbackCompatible_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) 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 : FirstObj P X
⊢ Arrows.Compatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
Arrows.pullbackCompatible_iff

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 : FirstObj P X
⊢ Arrows.PullbackCompatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_3.e'_2.e'_3
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
⊢ u = shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv u)

Tactic:
Equiv.symm_apply_apply

Goal state after:
case e'_3.e'_2.e'_3
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
⊢ u = u
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))),
      Arrows.Compatible P π
          ((equivShrink ((i : I) → P.obj (op (X i)))).symm ((equivShrink ((j : I) → P.obj (op (X j)))) 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)

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)

Tactic:
rintro h ⟨E, π⟩
    let eqv := conesEquivSieveCompatibleFamily P S (op E)
    constructor
    rw [← eqv.left_inv π]
    intro f₁ f₂
    let eqv' := homEquivAmalgamation (eqv π).2
    apply eqv'.injective
    ext
    apply h _ (eqv π).1 <;> exact (eqv' _).2

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
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ e (e.symm ((ConcreteCategory.hom (P₂.map f.op)) x)) = e ((ConcreteCategory.hom (P₁.map f.op)) (e.symm x))

Tactic:
by simp only [Equiv.apply_symm_apply, he]

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

Goal state before:
pp: 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 ⋯
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap
        (J.diagramNatTrans
          { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ } (unop X)) =
    colimit.ι (J.diagram P (unop X)) S ≫
      ⊤.toMultiequalizer (J.plusObj P) ≫ colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)

Tactic:
ι_colimMap,

Goal state after:
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 ⋯
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S =
    colimit.ι (J.diagram P (unop X)) S ≫
      ⊤.toMultiequalizer (J.plusObj P) ≫ colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)
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 : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ (fun i ↦ g i ≫ inv f) i₁ = g₂ ≫ (fun i ↦ g i ≫ inv 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:
simp only [← cancel_mono f, assoc, IsIso.inv_hom_id, comp_id] at h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P g)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)