mathlib-initiative/mathlib-tactics huggingface dataset:
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
X : B
⊢ F'.map (adj₂.unit.app (U.1 X)) ≫ adj₂.counit.app (F'.obj (U.1 X)) = 𝟙 (F'.obj (U.obj X))

Tactic:
adj₂.left_triangle_components

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
X : B
⊢ 𝟙 (F'.obj (U.obj X)) = 𝟙 (F'.obj (U.obj 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))
this : (X : (comonadicAdjunction F).toComonad.Coalgebra) →
  RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X) :=
  fun X ↦
    ⋯.mpr
      { Z := (comonadicAdjunction F).toComonad.cofree.obj ((comonadicAdjunction F).toComonad.obj X.A),
        left := Comonad.CofreeEqualizer.topMap X, right := Comonad.CofreeEqualizer.bottomMap X, w := ⋯,
        isLimit := Comonad.beckCoalgebraEqualizer X }
⊢ L'.IsLeftAdjoint

Tactic:
exact isLeftAdjoint_triangle_lift L' (Comonad.adj _) this

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ (normalizeAux nil (f.comp g)).comp (normalizeAux nil g✝) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))

Tactic:
ihf f,

Goal state after:
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g✝) =
    (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)

Tactic:
by
  induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
by
          rw [← whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
by
          rw [← whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
by
          rw [← whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
W✝ X✝ Y✝ Z✝ : ∫ᶜ F
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber ≫ eqToHom ⋯

Tactic:
· simp [← NatTrans.naturality_assoc, F.mapComp_assoc_right_inv_app, Strict.associator_eqToIso]

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
⊢ { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso } = 𝟙 { of := m α.of }

Tactic:
by ext x; exact congr_fun (EquivFunctor.map_refl' _) x

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a✝¹ a : B
t : a ⟶ a
inst✝ : Comonad t
a✝ b✝ c✝ d✝ : LocallyDiscrete (Discrete Unit)
x✝² : a✝ ⟶ b✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ 𝟙 t ≫ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
by
    rw [Category.id_comp]
    apply Comonad.comul_assoc

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u

Tactic:
by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₁ f₁₃ f ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
F.mapComp'_comp_whiskerLeft_mapComp'_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ F.mapComp' f₀₂ f₂₃ f ⋯ ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ =
    F.mapComp' f₀₂ f₂₃ f ⋯ ≫
      F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : TransitiveRelation p₁ p₂
x₁ x₂ x₃ : X
⊢ Rel.ofPair p₁ p₂ x₁ x₂ → Rel.ofPair p₁ p₂ x₂ x₃ → Rel.ofPair p₁ p₂ x₁ x₃

Tactic:
by
    refine fun ⟨r, ⟨hr₁, hr₂⟩⟩ ⟨r', ⟨hr₁', hr₂'⟩⟩ =>
      ⟨e.t ((PullbackCone.IsLimit.equivPullbackObj e.isLimit).symm ⟨(r, r'), hr₂.trans hr₁'.symm⟩),
        ⟨?_, ?_⟩⟩
    all_goals simpa

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
⊢ ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = τ

Tactic:
have h₁ : IsHomLift p (h ≫ f ≫ g) (τ ≫ ψ) := by simpa using IsHomLift.comp p (h ≫ f) _ τ ψ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∃! χ, p.IsHomLift h χ ∧ χ ≫ φ = τ
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
      eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j')
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
        eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map f).obj (Under.mk (𝟙 j'))) ≫
        eHomWhiskerRight V (F₁.map f) (F₂.obj j')

Tactic:
rw [this]

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
      eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j')
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫
        eHomWhiskerRight V (F₁.map f) (F₂.obj j') =
    s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map f).obj (Under.mk (𝟙 j'))) ≫
        eHomWhiskerRight V (F₁.map f) (F₂.obj j')
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
LF : D ⥤ H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst✝ : LF.IsLeftDerivedFunctor α W
this :
  α =
    L.whiskerLeft (LF.leftDerivedUnique (Localization.lift F hF L) (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom
⊢ IsIso α

Tactic:
rw [this]

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
LF : D ⥤ H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst✝ : LF.IsLeftDerivedFunctor α W
this :
  α =
    L.whiskerLeft (LF.leftDerivedUnique (Localization.lift F hF L) (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom
⊢ IsIso
    (L.whiskerLeft (LF.leftDerivedUnique (Localization.lift F hF L) (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj

Tactic:
by
  let e : F.obj (X ⨿ Y) ≃ F.obj X ⊕ F.obj Y := Iso.toEquiv
    <| (PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm.trans
    <| Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))
  rw [← Nat.card_sum]
  exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
X Y Z : C
inst✝² : IsConnected X
inst✝¹ : IsGalois Y
inst✝ : IsGalois Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
refine funext fun σ ↦ autMap_unique _ σ _ ?_
  rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (c₁.inj val✝ ≫
      bc.inl ≫
        IsColimit.desc h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯) =
    s.inj (Sum.inl val✝)

Tactic:
erw [h.fac]

Goal state after:
case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ c₁.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.left } =
    s.inj (Sum.inl val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (c₂.inj val✝ ≫
      bc.inr ≫
        IsColimit.desc h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯) =
    s.inj (Sum.inr val✝)

Tactic:
erw [h.fac]

Goal state after:
case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ c₂.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.right } =
    s.inj (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
A : PointedGaloisObject F
⊢ ↑f A = ↑g A

Tactic:
exact h A

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X)) =
    (Paths.lift (Symmetrify.lift φ)).map f.toPath ≫ (Symmetrify.lift φ).map (reverse f)

Tactic:
Paths.lift_toPath,

Goal state after:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X)) =
    (Symmetrify.lift φ).map f ≫ (Symmetrify.lift φ).map (reverse f)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e

Tactic:
· rintro h
    suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
      simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
    apply S.mul (S.inv hf) h

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ Groupoid.inv p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj c✝)}

Tactic:
by rw [mem_ofPred, inv_eq_inv, φ.map_inv, ← inv_eq_inv]; exact S.inv hp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
· rintro h _ _ g ⟨a, gφS⟩
    exact h gφS

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ ∃ φ, φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃

Tactic:
refine ⟨φ, ?_, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = g₁

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₂ = g₂

case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = g₃
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
x✝¹ x✝ : (j : J) × (F.obj (op j)).obj j
⊢ Types.coendRel F x✝¹ x✝ →
    (match x✝¹ with
      | ⟨j, y⟩ => Quot.mk (Types.coendRel G) ⟨j, (hom ((f.app (op j)).app j)) y⟩) =
      match x✝ with
      | ⟨j, y⟩ => Quot.mk (Types.coendRel G) ⟨j, (hom ((f.app (op j)).app j)) y⟩

Tactic:
rintro ⟨g, y⟩
        apply Quot.sound
        rw [Types.coendRel_iff]
        refine ⟨g, (f.app _).app _ y, ?_, ?_⟩
        · simp only [← NatTrans.comp_app_apply, f.naturality]
        · simp [← NatTrans.naturality_apply]

Goal state after: