mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
| (∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c))) ↔ ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))

Tactic:
lhs; intro c d; rw [isIso_iff_isIso_yoneda_map]

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
c : C
d : D
| ∀ (c_1 : D), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op c_1))
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
by
  refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩
  · have := lift (lift a b) c ≫= h
    simp only [lift_whiskerRight_assoc] at this
    simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]
    cat_disch
  · replace h := h (fst (R ⊗ R) R ≫ fst _ _) (fst _ _ ≫ snd _ _) (snd _ _)
    simp only [Hom.mul_def, Hom.add_def] at h
    convert! h using 2
    · cat_disch
    · ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : MonoidalCategory V
inst✝² : BraidedCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
x y : C
⊢ (unit G F).app (x, y) ≫ (braiding F G).inv.app (x ⊗ y) =
    (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)).inv ≫
      (unit F G).app (y, x) ≫ (F ⊛ G).map (β_ (y, x).2 (y, x).1).inv

Tactic:
change
    (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _
  simp [braiding, braidingHomCorepresenting, -tensor_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ ≫
        ℌ.π c' j =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      ℌ.π c j ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
        (H.obj c) (ℌ.π c) (ℌ.hπ c),

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ ≫
        ℌ.π c' j =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
⊢ P.ind f

Tactic:
have : P.underObj ≤ ObjectProperty.isFinitelyPresentable.{w} (Under X) := fun f hf ↦ hp _ hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
this : P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)
⊢ P.ind f
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
⊢ ∀ {d₁ d₂ d₁' d₂' : D} (f₁ : d₁ ⟶ d₁') (f₂ : d₂ ⟶ d₂') (x y : C),
    (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x, y) ≫ ((ι C V D).map (f₁ ⊗ₘ f₂)).app (x ⊗ y) =
      (((ι C V D).map f₁).app x ⊗ₘ ((ι C V D).map f₂).app y) ≫
        (DayConvolution.unit ((ι C V D).obj d₁') ((ι C V D).obj d₂')).app (x, y)

Tactic:
intros d₁ d₁' d₂ d₂' f f' x y

Goal state after:
C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
x y : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₁')).app (x, y) ≫ ((ι C V D).map (f ⊗ₘ f')).app (x ⊗ y) =
    (((ι C V D).map f).app x ⊗ₘ ((ι C V D).map f').app y) ≫
      (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₂')).app (x, y)
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty (X ≅ Y)

Tactic:
← isIso_iff_nonzero

Goal state after:
case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : IsIso f
⊢ Nonempty (X ≅ Y)
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
x✝ : (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
k : J
x y : ↑(F.obj k)
hx' : (ConcreteCategory.hom (c.ι.app k)) x = (ConcreteCategory.hom (c.ι.app j)) x'
hy' : (ConcreteCategory.hom (c.ι.app k)) y = (ConcreteCategory.hom (c.ι.app j)) y'
l : J
f : k ⟶ l
g : j ⟶ l
hl : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
l' : J
f' : k ⟶ l'
g' : j ⟶ l'
hl' : (ConcreteCategory.hom (F.map f')) y = (ConcreteCategory.hom (F.map g')) y'
m : J
a : l ⟶ m
h : (ConcreteCategory.hom (F.map (f ≫ a))) x ≤ (ConcreteCategory.hom (F.map (f ≫ a))) y
b : l' ⟶ m
h₁ : f ≫ a = f' ≫ b
h₂ : g ≫ a = g' ≫ b
⊢ (ConcreteCategory.hom (F.map (f ≫ a))) y = (ConcreteCategory.hom (F.map (g ≫ a))) y'

Tactic:
simp [h₁, h₂, hl']

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
hA : HasCardinalLT (↑Set.univ) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨Set.univ, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨Set.univ, hA⟩)) f = 𝟙 X
⊢ HasCardinalLT X κ

Tactic:
exact (hasCardinalLT_iff_of_equiv (Equiv.Set.univ X) _).1 hA

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y✝ : C
f : Y✝ ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y✝ := fun a ↦ pullback.fst f (π a)
Y : C
a : α
⊢ S (π a)

Tactic:
rw [hS]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y✝ : C
f : Y✝ ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y✝ := fun a ↦ pullback.fst f (π a)
Y : C
a : α
⊢ Presieve.ofArrows Z π (π a)
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
i j : J
f : i ⟶ j
hf : (D₃ D m₁).W f
⊢ (D₃ D m₁).P j

pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P m₁

Tactic:
· exact (D₃ D m₁).tgt hf

Goal state after:
case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
X Y j : J
hj : D.P j
⊢ (D₃ D m₁).P m₁
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ D₁.hom (r ≫ q ≫ f i) r' (r ≫ a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a' (r ≫ a ≫ p' j) (r ≫ a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (r ≫ q ≫ f i) (r ≫ a ≫ p' j) r' ⋯ ⋯ =
    pullHom (mor w φ q a fac) r r' r' ⋯ ⋯

Tactic:
mor_eq _ _ _ _ _ _ _ rfl rfl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ D₁.hom (r ≫ q ≫ f i) r' (r ≫ a ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) a' (r ≫ a ≫ p' j) (r ≫ a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (r ≫ q ≫ f i) (r ≫ a ≫ p' j) r' ⋯ ⋯ =
    pullHom
      (D₁.hom (q ≫ f i) q (a ≫ p' j) ⋯ ⋯ ≫
        pullHom (φ.hom j) a (a ≫ p' j) (a ≫ p' j) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a ≫ p' j) q ⋯ ⋯)
      r r' r' ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂

Tactic:
mor_eq _ _ _ _ _ _ _ rfl rfl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    mor w φ q a₂ fac₂
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    mor w φ q a₂ fac₂

Tactic:
mor_eq _ _ _ _ _ _ _ rfl rfl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ p ≫ (sq i i).p = f i

Tactic:
rw [← (sq i i).hp₁, reassoc_of% h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
⊢ PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks =
    PreOneHypercover.Hom.id E.toPreOneHypercover

Tactic:
by
  refine PreOneHypercover.Hom.ext' rfl (by simp) (by simp) (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y))) = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
congr; simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B →
    A ≤ B

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ A ≤ B →
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B

Tactic:
· intro h
      have : range (Subobject.mk A.ι).arrow ≤ range (Subobject.mk B.ι).arrow :=
        leOfHom (((equivalenceMonoOver F).trans
          (ThinSkeleton.equivalence _).symm).inverse.map (homOfLE h))
      simpa using this

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ A ≤ B →
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      ((Ext.mk₀ biprod.fst).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).1
          ⋯ +
        (Ext.mk₀ biprod.snd).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).2
          ⋯)
      ⋯ =
    (ConcreteCategory.hom (S.fromBiprod F n))
      ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))

Tactic:
fromBiprod_biprodIsoProd_inv_apply

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      ((Ext.mk₀ biprod.fst).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).1
          ⋯ +
        (Ext.mk₀ biprod.snd).comp
          ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
              ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv) (x₂, x₃))).2
          ⋯)
      ⋯ =
    (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₂.op)) x₂ -
      (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₁₃.op)) x₃
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

Tactic:
exact Presheaf.isPullback_χ_truth m.hom

Goal state after: