mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j j'✝ : C
hj₂ : cofilteredClosure f j'✝
ih' : ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := j'✝, property := hj₂ }.obj
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
g g' : CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶ j'✝
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := eq g g', property := ⋯ }.obj

Tactic:
rcases ih' with ⟨⟨m, y⟩, rfl⟩

Goal state after:
case eq
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := eq g g', property := ⋯ }.obj
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasLimitsOfShape (Discrete J) C
⊢ ObjectProperty.strictLimitsOfShape IsIndObject (Discrete J) ≤ IsIndObject

Tactic:
by
    rintro _ ⟨F, hF⟩
    exact isIndObject_limit_of_discrete_of_hasLimitsOfShape _ hF

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v b : ↥S
⊢ b ∈ S.attach → b ≠ v → Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0

Tactic:
hb

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v b : ↥S
hb : b ∈ S.attach
⊢ b ≠ v → Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
⊢ b ∈ (Opposite.unop S).attach → b ≠ v → Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

Tactic:
hb

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
⊢ b ≠ v → Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ R.ι'.f 0 =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
dsimp [ι']

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv.f 0 ≫
      (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat).f 0 =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ QuasiIso R.ι'

Tactic:
dsimp [ι']

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ QuasiIso
    ((HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv ≫
      HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
⊢ kernel.ι (factorThruImage (d g)) ≫ d f = 0

Tactic:
← kernelFactorThruImage_hom_comp_ι,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
⊢ ((kernelFactorThruImage (d g)).hom ≫ kernel.ι (d g)) ≫ d f = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
⊢ P ≤ F.kernel

Tactic:
intro X

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
⊢ P X ≤ F.kernel X
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
⊢ (ofObjectProperty P Q).map F ≤ ofObjectProperty (P.map F) (Q.map F)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), (ofObjectProperty P Q).map F f → ofObjectProperty (P.map F) (Q.map F) f
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ ∀ {Y Z : C} (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : Y ⟶ Z), isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
X : C
⊢ ∀ {Y Z : C} (i : Y ⟶ Z), isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ Epi (L.map f)

Tactic:
Preadditive.epi_iff_cancel_zero

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ ∀ (R : D) (g : L.obj Y ⟶ R), L.map f ≫ g = 0 → g = 0
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ : G
⊢ { hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } =
    { hom := FintypeCat.homMk (Quotient.lift (fun σ_1 ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ } *
      { hom := FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ }

Tactic:
by
    apply Action.hom_ext
    ext (x : G ⧸ N)
    induction x using Quotient.inductionOn with | _ x
    change ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
    rw [mul_inv_rev, mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
x✝ : Mono f
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
intro X

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y : D
f : X✝ ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
x✝ : Mono f
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Epi (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
intro X

Goal state after:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y : D
f : X✝ ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
x✝ : Epi f
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
a✝ : R
x✝¹ y✝ : F ⟶ G
x✝ : C
⊢ (a✝ • (x✝¹ + y✝)).app x✝ = (a✝ • x✝¹ + a✝ • y✝).app x✝

Tactic:
apply smul_add

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ w)

Goal state after:
case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ w = φ.map L ⋯
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
have w := comm g =≫ f.inv; simp at w; simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
⊢ ∀ (X : B) (Y Y' : A) (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g

Tactic:
intro X

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
⊢ ∀ (Y Y' : A) (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y' X) (h_1 ≫ g) =
      (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) h_1 ≫ R.map g
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
⊢ ∀ (X' X : C) (Y : B) (f : X' ⟶ X) (g : L.obj X ⟶ Y),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X' Y).symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y).symm g

Tactic:
intro X

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
X : C
⊢ ∀ (X_1 : C) (Y : B) (f : X ⟶ X_1) (g : L.obj X_1 ⟶ Y),
    (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y).symm (L.map f ≫ g) =
      f ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h X_1 Y).symm g
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Tactic:
intro X

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
⊢ (X : (comonadicAdjunction F).toComonad.Coalgebra) → RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X)

Tactic:
intro X

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
X : (comonadicAdjunction F).toComonad.Coalgebra
⊢ RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X)
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : ↑⟨some b, hb⟩ = ↑⟨some w, ⋯⟩
⊢ some b = (partialFunToPointed.map f).toFun (some a)

Tactic:
dsimp at h

Goal state after:
case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
x✝ : ∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩
w : Y✝
hw : w ∈ f a
h : some b = some w
⊢ some b = (partialFunToPointed.map f).toFun (some a)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
b✝ : β
e : (f a).get h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

Tactic:
injection h₂.symm.trans e with h

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
b✝ : β
e : (f a).get h₁ = Sum.inl b✝
h : b = b✝
⊢ b ∈ Part.some b✝
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
⊢ (CostructuredArrow.toOver L' (R'.obj b)).Final

Tactic:
dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
⊢ (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).Final
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X : ↑s.pt), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X

Tactic:
intro X

Goal state after:
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
⊢ (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
intro X

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
⊢ ∀ (Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
Y : Over X
⊢ (mapPullbackAdj (𝟙 X)).unit.app Y ≫ (pullbackId X).hom.app ((map (𝟙 X)).obj Y) = (mapPullbackAdj (𝟙 X)).unit.app Y

Tactic:
by
  rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom_app]

Goal state after: