mathlib-initiative/mathlib-tactics huggingface dataset:
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 F G).app (x, y) ≫ (braiding F G).hom.app (x ⊗ y) =
    (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)).hom ≫
      (unit G F).app (y, x) ≫ (G ⊛ F).map (β_ (y, x).1 (y, x).2).hom

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

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
hS : ∀ (i : E.I₀), ∃ 𝒰, S i = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
choose F hF using hS

Goal state after:
case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
i : ι
⊢ o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i

Tactic:
ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩
  simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
  simp only [Matrix.mul_apply, Limits.biproduct.components,
    HomOrthogonal.matrixDecomposition_apply, Category.comp_id, Category.id_comp, Category.assoc,
    End.mul_def, eqToHom_refl, eqToHom_trans_assoc]
  conv_lhs => rw [← Category.id_comp w, ← biproduct.total]
  simp only [Preadditive.sum_comp, Preadditive.comp_sum]
  apply Finset.sum_congr_set
  · simp
  · intro b nm
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
    simp only [Category.assoc]
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    convert! comp_zero
    simp only [o.eq_zero nm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag

Tactic:
ext <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : ¬End.of f - (algebraMap 𝕜 (End X)) c ≠ 0
⊢ c • 𝟙 X = f

Tactic:
Ne,

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : ¬¬End.of f - (algebraMap 𝕜 (End X)) c = 0
⊢ c • 𝟙 X = f
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case pos
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✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1

Tactic:
exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ : Mat_ C
f : X✝.Hom Y✝
⊢ (Hom.id X✝).comp f = f

Tactic:
by
    classical
    simp +unfoldPartialApp [dite_comp]

Goal state after:
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
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
h₇ : x₃ = y₃
⊢ x = y

Tactic:
exact hx₁.symm.trans ((ConcreteCategory.congr_hom (c.w a) x₁).symm.trans
      ((congr_arg (c.ι.app l) (h₃.symm.trans (h₇.trans h₅))).trans
        ((ConcreteCategory.congr_hom (c.w a) y₁).trans hy₁)))

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ (additiveObjIsoBiproduct F M).inv ≫ F.map f =
    (biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : f ≫ g₁ ≫ p.ι.app j₁ = f ≫ g₂ ≫ p.ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv : f ≫ g₁ ≫ p.diag.map u = f ≫ g₂ ≫ p.diag.map v
⊢ g₁ ≫ p.ι.app j₁ = g₂ ≫ p.ι.app j₂

Tactic:
rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
⊢ ∀ {i j : J} {f : i ⟶ j}, (D₁.W ⊔ D₂.W) f → (D₁.P ⊔ D₂.P) i

Tactic:
rintro _ _ _ (h | h)
    · exact Or.inl (D₁.src h)
    · exact Or.inr (D₂.src h)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
g : Z ⟶ T
f : (d : D₁ W Z) → (↑d.fst).right ⟶ T
hf : ∀ (d : D₁ W Z), (fun g ↦ (↑d.fst).hom ≫ g) (f d) = d.snd ≫ g
d : (D₂.multispanShape W Z).L
⊢ (fun g ↦ (↑d.fst).hom ≫ g)
      ((D₂.multispanIndex W Z).fst d ≫
        match (D₂.multispanShape W Z).fst d with
        | PUnit.unit => pushout.desc (Sigma.desc f) g ⋯) =
    (fun g ↦ (↑d.fst).hom ≫ g)
      ((D₂.multispanIndex W Z).snd d ≫
        match (D₂.multispanShape W Z).snd d with
        | PUnit.unit => pushout.desc (Sigma.desc f) g ⋯)

Tactic:
simp [reassoc_of% d.2.2]

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalLocallyPresentable (Type u) κ

Tactic:
rw [IsCardinalLocallyPresentable.iff_exists_isStrongGenerator]
  exact ⟨.singleton PUnit, inferInstance, isStrongGenerator_punit, by
    simp only [ObjectProperty.singleton_le_iff,
      CategoryTheory.isCardinalPresentable_iff, isCardinalPresentable_iff]
    exact hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out)⟩

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Cᵒᵖ ⥤ Type w
e : F ≅ F'
⊢ F'.IsRepresentedBy ((ConcreteCategory.hom (e.hom.app (op X))) x)

Tactic:
by
  rw [iff_exists_representableBy]
  use h.representableBy.ofIso e
  simp [RepresentableBy.ofIso]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Presieve S
hR : Sieve.generate R ∈ J S
⊢ F.IsStackFor R

Tactic:
by
  simpa using F.isStackFor' _ hR

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ φ.hom i = φ'.hom i

Tactic:
refine F.presheafHomObjHomEquiv.injective ?_i

Goal state after:
case _i
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
⊢ F.presheafHomObjHomEquiv (φ.hom i) = F.presheafHomObjHomEquiv (φ'.hom i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map (g.h₀ i ≫ f.h₀ (g.s₀ i)).op = t.ι i

Tactic:
← h1,

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map (hgf.a i ≫ F.p₁ (hgf.H i)).op = t.ι i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
⊢ m = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
refine Multifork.IsLimit.hom_ext hE fun i ↦ ?_

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ m ≫ (E.multifork G).ι i = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ (E.multifork G).ι i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ (cylinder f g).toPullback k ≫ pullback.fst ((cylinder f g).f i) ((cylinder f g).f j) =
    pullback.fst
        (pullback.map (cylinderf f g i.snd) (cylinderf f g j.snd) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.fst ((cylinder f g).f i) ((cylinder f g).f j)

Tactic:
simp [toPullback]

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ (cylinder f g).toPullback k ≫ pullback.snd ((cylinder f g).f i) ((cylinder f g).f j) =
    pullback.fst
        (pullback.map (cylinderf f g i.snd) (cylinderf f g j.snd) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.snd ((cylinder f g).f i) ((cylinder f g).f j)

Tactic:
simp [toPullback]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this✝ : (F.toDescentData f).Faithful
this : (F.toDescentData f).Full
⊢ (F.toDescentData f).IsEquivalence

Tactic:
have : (F.toDescentData f).EssSurj := ⟨fun D ↦
    ⟨_, ⟨h.preimageIso (e.app _ ≪≫ (F.toDescentData f').objObjPreimageIso (H.obj D))⟩⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this✝¹ : (F.toDescentData f).Faithful
this✝ : (F.toDescentData f).Full
this : (F.toDescentData f).EssSurj
⊢ (F.toDescentData f).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ ((Over.forget (unop (op X))).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M)).map φ ≫
      uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j').hom.op)) =
    uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)) ≫
      ((Over.forget (unop (op X))).op ⋙ G).map φ

Tactic:
by
        dsimp
        rw [tensorHom_id, ← uncurry_natural_right, ← uncurry_pre_app, Category.assoc,
          Category.assoc, ← enrichedOrdinaryCategorySelf_eHomWhiskerRight,
          ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
        congr 2
        exact (enrichedHom_condition A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)
          (i := Under.mk j.unop.hom.op) (j := Under.mk j'.unop.hom.op)
            (Under.homMk φ.unop.left.op (Quiver.Hom.unop_inj (by simp)))).symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : MonoidalCategory A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
X : C
x : Φ.fiber.obj X
G₁ G₂ : Cᵒᵖ ⥤ A
⊢ (Φ.toPresheafFiber X x G₁ ⊗ₘ Φ.toPresheafFiber X x G₂) ≫ LaxMonoidal.μ Φ.presheafFiber G₁ G₂ =
    Φ.toPresheafFiber X x (G₁ ⊗ G₂)

Tactic:
simp [← cancel_mono (OplaxMonoidal.δ Φ.presheafFiber G₁ G₂)]

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
⊢ (ConcreteCategory.hom (χ'.app X)).toFun x = (ConcreteCategory.hom ((χ m).app X)).toFun x

Tactic:
refine Sieve.ext fun Y f => ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ ((ConcreteCategory.hom (χ'.app X)).toFun x).arrows f ↔ ((ConcreteCategory.hom ((χ m).app X)).toFun x).arrows f
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
have : G.Additive := adj.right_adjoint_additive

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : (F.mapTriangle.obj (Triangle.mk (G.map T.mor₁) f g)).obj₃ ⟶ T.obj₃
h₁ : (F.mapTriangle.obj (Triangle.mk (G.map T.mor₁) f g)).mor₂ ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  (F.mapTriangle.obj (Triangle.mk (G.map T.mor₁) f g)).mor₃ ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
dsimp at h h₁ h₂ ⊢

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  (F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁)) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
⊢ Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ∈
    distinguishedTriangles