mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).hom

Tactic:
let : F.Monoidal := functorMonoidalOfComp L W F G

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).hom
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
I : C
inst✝ : Closed I
A : C
⊢ toUnit A ≫ curryRightUnitorHom I = curry (fst I A)

Tactic:
apply uncurry_injective
  simp [uncurry_natural_left, curryRightUnitorHom, fst_def, toUnit]

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✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))

Tactic:
· change IsIso ((comparisonAdjunction adj).unit.app X).f
        rw [comparisonAdjunction_unit_f]
        exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CartesianMonoidalCategory C
G H K : C
inst✝² : GrpObj G
inst✝¹ : GrpObj H
inst✝ : GrpObj K
φ : H ⟶ G
⊢ toUnit (G ⊗ 𝟙_ C) ≫ η = G ◁ η ≫ conj G

Tactic:
simp [conj, comp_mul, comp_inv, toUnit_unique _ (toUnit _), ← Hom.one_def]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
ψ : G ⊗ H ⟶ H
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ (monoidHom φ X) (lift z x ≫ ψ) = z * (monoidHom φ X) x * z⁻¹

Tactic:
simp [hψ]

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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
⊢ η ≫ ℌ'.coev_app = ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ'

Tactic:
ext 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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
⊢ (η ≫ ℌ'.coev_app).app c = (ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c
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 H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
⊢ ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ = 𝟙 H

Tactic:
ext 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 H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
c : C
⊢ (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c = (𝟙 H).app c
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
⊢ X.normalizeObj n = Y.normalizeObj n

Tactic:
by
  rcases f with ⟨f'⟩
  apply @congr_fun _ _ fun n => normalizeObj X n
  clear n f
  induction f' with
  | comp _ _ _ _ => apply Eq.trans <;> assumption
  | whiskerLeft _ _ ih => funext; apply congr_fun ih
  | whiskerRight _ _ ih => funext; apply congr_arg₂ _ rfl (congr_fun ih _)
  | @tensor W X Y Z _ _ ih₁ ih₂ =>
      funext n
      simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]
  | _ => funext; rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ Δ ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
rw [Bimon.one_comul_assoc, tensorHom_def_assoc, unitors_inv_equal,
    ← rightUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc] at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
⊢ (ι C V D).map (ρ_ d).hom = (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom

Tactic:
apply corepresentableByRight
    (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.homEquiv.injective
  dsimp
  ext ⟨x, _⟩
  dsimp [corepresentableByRight]
  simp only [id_whiskerRight, Category.id_comp,
    DayConvolutionUnit.rightUnitor_hom_unit_app]
  exact rightUnitor_hom_unit_app V d x

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom n = (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom m
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (G.obj n).obj.hom = Subobject.mk (G.obj m).obj.hom

Tactic:
exact hn m (leOfHom hm)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ IsIso (Hom.right (π f))

Tactic:
simp only [π, homMk_right]

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ IsIso (𝟙 v.right)
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
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
d' : l₂ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₂ ≫ d'))) y'
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
⊢ (ConcreteCategory.hom (F.map (b₁ ≫ d))) x ≤ (ConcreteCategory.hom (F.map (b₂ ≫ d'))) y

Tactic:
simpa [← hl₁, ← hl₂] using h

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) i

Tactic:
rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) j_1

Tactic:
rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
⊢ Mono (coequalizer.desc f ⋯)

Tactic:
apply (IsKernelPair.of_hasPullback _).mono_of_eq_fst_snd

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
⊢ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Tactic:
choose Y' π' _ H using b h₂

Goal state after:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h✝ : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : (extensiveCoverage C).Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → (extensiveCoverage C).Saturate Y (Sieve.pullback f S)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), R.arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Tactic:
choose β _ Y_n π_n H using fun a => b (h' a)

Goal state after:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : (extensiveCoverage C).Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → (extensiveCoverage C).Saturate Y (Sieve.pullback f S)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H :
  ∀ (a : α), Nonempty (IsColimit (Cofan.mk (Y₁ a) (π_n a))) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u_2
inst✝³ : Category.{v_2, u_2} A
S✝¹ : C
E✝¹ : PreZeroHypercover S✝¹
inst✝² : E✝¹.HasPullbacks
S✝ : C
E✝ : PreZeroHypercover S✝
inst✝¹ : E✝.HasPullbacks
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
rw [toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks]
      exact E.toPreOneHypercoverHomotopy

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
Y : C
hx : x.Compatible
g : Y ⟶ X
⊢ ∃ φ,
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
let c : Cone ((Presieve.diagram (Sieve.pullback g S).arrows).op ⋙ G) :=
    { pt := F.obj (op Y)
      π :=
        { app := fun ⟨Z, hZ⟩ => F.map Z.hom.op ≫ (x _ hZ).app (op (Over.mk (𝟙 _)))
          naturality := by
            rintro ⟨Z₁, hZ₁⟩ ⟨Z₂, hZ₂⟩ ⟨⟨f : Z₂ ⟶ Z₁⟩⟩
            dsimp
            rw [id_comp, assoc]
            have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)
            simp only [op_id, Functor.map_id, id_apply] at H
            let φ : Over.mk f.left ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk f.left
            have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
            dsimp at H H' ⊢
            erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f] } }

Goal state after:
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
Y : C
hx : x.Compatible
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun x_1 ↦
          match x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
⊢ ∃ φ,
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ G.IsGeneratedBy fun i' ↦ x (e i')

Tactic:
isGeneratedBy_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ ⨆ i, ofSection (x (e i)) = G
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
⊢ (m.hom ≫ Subfunctor.lift (Presheaf.χ m.hom) ⋯) ≫ (closedSieves J).ι =
    (((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Subfunctor.lift (Presheaf.truth C) ⋯) ≫
      (closedSieves J).ι

Tactic:
simpa using Presheaf.comp_χ_eq _

Goal state after:
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
⊢ G.mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
obtain ⟨h, ⟨h₁, h₂⟩⟩ := complete_distinguished_triangle_morphism _ _
      (F.map_distinguished _ mem) hT (adj.counit.app T.obj₁) (adj.counit.app T.obj₂) (by simp)

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.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
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
⊢ ∃ k, πQ f₂ β ≫ k = x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := Triangle.yoneda_exact₂ _ hT (ι.map x₂) (by simp [← ι.map_comp, hx₂])

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
⊢ ∃ k, πQ f₂ β ≫ k = x₂
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map f (map g s)).prod = (map f (map g t)).prod ↔ s.prod = t.prod

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A

Tactic:
map_map,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map (f ∘ g) s).prod = (map f (map g t)).prod ↔ s.prod = t.prod

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A