mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))

Tactic:
apply IsReflexivePair.mk' (F.map (adj.unit.app _)) _ _
  · rw [← F.map_comp, ← F.map_id]
    exact congr_arg F.map A.unit
  · dsimp
    rw [adj.left_triangle_components]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ { f // F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f } ≃
    { g // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g }

Tactic:
refine (adj.homEquiv _ _).subtypeEquiv ?_
      intro f
      rw [← (adj.homEquiv _ _).injective.eq_iff, Adjunction.homEquiv_naturality_left,
        adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp]
      dsimp
      rw [adj.right_triangle_components_assoc, ← G.map_comp, F.map_comp, Category.assoc,
        adj.counit_naturality, adj.left_triangle_components_assoc]
      apply eq_comm

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ CreatesColimit (parallelPair f g) G

Tactic:
apply +allowSynthFailures monadicCreatesColimitOfPreservesColimit
    -- Porting note: oddly +allowSynthFailures had no effect here and below
  all_goals
    apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
    dsimp
    infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X = 𝟙 X

Tactic:
by
      rw [braiding_naturality_right, ← braiding_inv_naturality_right]
      simp [monoidalComp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : LeftRigidCategory C
X : C
⊢ (ᘁ𝟙 X).op.mop = 𝟙 { unmop := op ᘁX }

Tactic:
by simp [leftAdjointMate_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Tor

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
inst✝³ : Abelian C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective Y
n : ℕ
⊢ IsZero (((Tor C (n + 1)).obj X).obj Y)

Tactic:
by
  apply Functor.isZero_leftDerived_obj_projective_succ

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Tor

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
inst✝³ : Abelian C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((Tor' C (n + 1)).obj X).obj Y)

Tactic:
by
  apply Functor.isZero_leftDerived_obj_projective_succ

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

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)

Tactic:
intro Y hY
    exact H _ hY

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P.localEpi ≤ P.isoClosure.localEpi

Tactic:
intro X Y f hf Z ⟨T, hT, ⟨e⟩⟩ u v huv

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u v : Y ⟶ Z
huv : (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v
⊢ u = v
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
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ leftAdd X Y x1 x2) 0

Tactic:
have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr := by
    intro f
    ext
    · simp
    · simp [Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ leftAdd X Y x1 x2) 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
⊢ (ObjectProperty.ofObj ι).isoClosure J

Tactic:
let e := Equiv.ofInjective _ f.injective

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
⊢ (ObjectProperty.ofObj ι).isoClosure J
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j,
        (fun x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
          if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
      ⟨i, j⟩ ⟨i', j'⟩ =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
Finset.sum_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ c,
        ((fun x y ↦ if h : x.fst = c then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
            if h : y.fst = c then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
          ⟨i, j⟩)
      ⟨i', j'⟩ =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
hc : IsColimit c
this : IsFiltered A
⊢ IsColimit ((coyoneda.obj (Opposite.op J)).mapCocone c)

Tactic:
have := IsCardinalFiltered.of_le A h

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
hc : IsColimit c
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
⊢ IsColimit ((coyoneda.obj (Opposite.op J)).mapCocone c)
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (∑ j, (fun j_1 x ↦ if h : j_1 = j then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : j = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

Tactic:
Finset.sum_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (∑ c, ((fun j x ↦ if h : j = c then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : c = k then eqToHom ⋯ else 0) i) j =
    if h : i = j then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (∑ c, ((fun j x ↦ if h : j = c then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : c = k then eqToHom ⋯ else 0) i) j =
    if h : i = j then eqToHom ⋯ else 0

Tactic:
Finset.sum_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∑ c, ((fun j x ↦ if h : j = c then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : c = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) (Order.succ j) A)) κ₂

Tactic:
have hκ₂ : κ₂.IsRegular := Fact.out

Goal state after:
case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) (Order.succ j) A)) κ₂
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) (Order.succ j) A)) κ₂

Tactic:
transfiniteIterate_succ _ _ _ hj,

Goal state after:
case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
⊢ HasCardinalLT (↑(φ Y m (transfiniteIterate (φ Y m) j A))) κ₂
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ EffectiveEpiFamily X_1 π},
      ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
        T.FactorsThruAlong S f

Tactic:
by
    rintro B₁ B₂ f S ⟨α, _, X₁, π₁, rfl, hS⟩
    obtain ⟨β, _, X₂, π₂, h, i, ι, hh⟩ := Precoherent.pullback f α X₁ π₁ hS
    refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩
    rintro _ _ ⟨b⟩
    exact ⟨(X₁ (i b)), ι _, π₁ _, ⟨_⟩, hh _⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f} →
    ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
⟨Z, π, hπ, h_epi⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
⊢ ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
⊢ ∃ j, ∀ (k : ι), D k ≤ j

Tactic:
let φ (x : (Σ (i : ι), (Subtype (D i).P))) : x.2.1 ⟶ m :=
      (D x.1).isTerminal.lift x.2.2 ≫ u x.1

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
⊢ ∃ j, ∀ (k : ι), D k ≤ j
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_4.inl.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
X Y : J
i✝ : Unit
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ 𝟙 m ≫ lj = li

Tactic:
exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩

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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
j : J
hj : D.P j
f : j ⟶ m₁
hf : (D₄ D φ).W f
⊢ f = φ ⟨j, hj⟩

Tactic:
obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
j : J
hj : D.P j
f : j ⟶ m₁
hf : D.W f
⊢ f = φ ⟨j, hj⟩

case inl.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Unit
hj : D.P m₁
⊢ 𝟙 m₁ = φ ⟨m₁, hj⟩

case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Subtype D.P
hj : D.P ↑i✝
⊢ φ i✝ = φ ⟨↑i✝, hj⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
X Y : J
i✝ : Unit
⊢ ∃ li lj, (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ 𝟙 m₁ ≫ lj = li

Tactic:
exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
· exact (e.sheafCongrPreregular A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.property

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
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 : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ pullHom (mor w φ Y₁.hom a₁ fac₁) g₁ Z.hom Z.hom ⋯ ⋯ =
    pullHom (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) ⋯) g₂ Z.hom Z.hom ⋯ ⋯

Tactic:
familyOfElements_eq _ _ _ _ fac₂,

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 : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ pullHom (mor w φ Y₁.hom a₁ fac₁) g₁ Z.hom Z.hom ⋯ ⋯ = pullHom (mor w φ Y₂.hom a₂ fac₂) g₂ Z.hom Z.hom ⋯ ⋯
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
⊢ ∀ ⦃X_1 Y : (Over (unop (op X)))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Over.forget (unop (op X))).op ⋙ F).map f ≫ app hG x hx (unop Y).hom =
      app hG x hx (unop X_1).hom ≫ ((Over.forget (unop (op X))).op ⋙ G).map f

Tactic:
rintro ⟨Y₁ : Over X⟩ ⟨Y₂ : Over X⟩ ⟨φ : Y₂ ⟶ Y₁⟩
          apply (hG Y₂.hom).hom_ext
          rintro ⟨Z : Over Y₂.left, hZ⟩
          dsimp
          rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]
          rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ),
            ← F.map_comp_assoc, op_comp]
          congr 3
          simp

Goal state after:
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₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 2 3 _proof_299✝ _proof_452✝ ≫ (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 2 3 _proof_299✝ _proof_452✝

Tactic:
by dsimp; rw [comp_id, id_comp]; rfl

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

Goal state before:
pp: case H
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 ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))

Tactic:
· simp only [ObjectProperty.ι_obj, terminal_obj, Ω_obj, ObjectProperty.ι_map, χ_hom, truth_hom]
    apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)
    · simp only [Category.comp_id]
      exact Presheaf.isPullback_χ_truth m.hom
    · simp_all

Goal state after: