mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V α.inv Y₁ ≫ eHomWhiskerRight V α.hom Y₁

pp: case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X β.inv

pp: case a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X β.hom

Tactic:
rw [← eHomWhiskerRight_comp]

Goal state after:
case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V (α.hom ≫ α.inv) Y₁

case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X β.inv

case a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X β.hom
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V α.hom Y ≫ eHomWhiskerRight V α.inv Y

pp: case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X₁ β.hom

pp: case a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X₁ β.inv

Tactic:
rw [← eHomWhiskerRight_comp]

Goal state after:
case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerRight V (α.inv ≫ α.hom) Y

case a.a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X₁ β.hom

case a
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
| eHomWhiskerLeft V X₁ β.inv
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom
⊢ F.map h.inv ≫ A₀.str = A₁.str ≫ h.inv

Tactic:
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
        simp

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst✝¹ : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst✝ : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
  infer_instance

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

Goal state before:
pp: case h.refine_2
𝒮 : 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) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)

Tactic:
· intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      simp [hπ'₂.symm]

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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
⊢ ∀ (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = φ'

Tactic:
g

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
⊢ ∀ (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

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

Tactic:
g

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
⊢ ∀ (φ' : c ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_2
𝒮 : 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.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
· intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      simp [hπ'₂.symm]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
b' : 𝒳
⊢ ∀ (g : S ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift (f ≫ g) φ'], ∃! χ, p.IsHomLift g χ ∧ φ.hom ≫ χ = φ'

Tactic:
g

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
⊢ ∀ (φ' : a ⟶ b') [p.IsHomLift (f ≫ g) φ'], ∃! χ, p.IsHomLift g χ ∧ φ.hom ≫ χ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case refine_1
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ homCartesianLift f g φ' ≫ cartesianLift a f = φ'

Tactic:
exact Hom.ext _ _ (by simpa using IsHomLift.fac (forget F) (g ≫ f) φ')
        (by simp [← Cat.Hom₂.comp_app])

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

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : ↑(F.obj { as := op S })
f : a ⟶ b
⊢ ∀ ⦃a₂ : a ⟶ b⦄, (Fiber.inducedFunctor ⋯).map f = (Fiber.inducedFunctor ⋯).map a₂ → f = a₂

Tactic:
g

Goal state after:
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : ↑(F.obj { as := op S })
f g : a ⟶ b
⊢ (Fiber.inducedFunctor ⋯).map f = (Fiber.inducedFunctor ⋯).map g → f = g
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ 𝟙 (L₁.obj (F.obj X₂)) ≫ β.app X₂ = β.app X₂

Tactic:
Category.id_comp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ β.app X₂ = β.app X₂
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
A X : C
inst✝ : IsConnected A
a : (F.obj A).obj
f : A ⟶ X
⊢ ∀ ⦃a₂ : A ⟶ X⦄,
    (fun f ↦ (ConcreteCategory.hom (F.map f)) a) f = (fun f ↦ (ConcreteCategory.hom (F.map f)) a) a₂ → f = a₂

Tactic:
g

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).obj
f g : A ⟶ X
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f)) a) f = (fun f ↦ (ConcreteCategory.hom (F.map f)) a) g → f = g
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
h : Nonempty (F.obj X).obj
⊢ ∃ A x, IsGalois A

Tactic:
obtain ⟨x⟩ := h
  obtain ⟨A, f, a, h1, _⟩ := exists_hom_from_galois_of_fiber F X x
  exact ⟨A, f, h1⟩

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ ∀ (g : X ⟶ Y), (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

Tactic:
g

Goal state after:
X Y : Type u
f g : X ⟶ Y
⊢ (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.obj
this : ∀ (i : ι), ContinuousSMul G (f i).V.obj
i : ι
x : (f i).V.obj
U : OpenSubgroup G := { toSubgroup := MulAction.stabilizer G x, isOpen' := ⋯ }
⊢ ∃ U, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))

Tactic:
exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
⊢ (of C ⋙ lift φ).toPrefunctor = φ.toPrefunctor

Tactic:
change Quiver.FreeGroupoid.of C ⋙q
      (Quotient.functor (FreeGroupoid.homRel C)).toPrefunctor ⋙q
        (lift φ).toPrefunctor = φ.toPrefunctor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
⊢ Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C)).toPrefunctor ⋙q (lift φ).toPrefunctor = φ.toPrefunctor
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ : c ⟶ c
⊢ 𝟙 c ≫ γ = γ

Tactic:
Category.id_comp

Goal state after:
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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))

Tactic:
rw [← Functor.map_id]

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ : C
p✝ : c✝ ⟶ c✝
h : p✝ ∈ S.arrows c✝ c✝
⊢ Groupoid.inv p✝ ∈ {f | c✝ = c✝ ∧ f ∈ S.arrows c✝ c✝}

Tactic:
exact ⟨rfl, S.inv h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Tactic:
let f₁ : (mk (Y := zero) (f ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
      homMk left

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk a := homMk WalkingParallelPairHom.left ⋯
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerRight (α_ f g h).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (α_ (mapPair f.toFunctor (𝟭 D)).toCatHom (mapPair g.toFunctor (𝟭 D)).toCatHom
                (mapPair h.toFunctor (𝟭 D)).toCatHom).hom ≫
            (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
by intros; exact congr($(mapWhiskerRight_associator_hom D _ _ _).toCatHom₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = 0
⊢ Cofork.π (c₁.map (F.flip.obj X₂)) ≫ (F.obj c₁.pt).map f₂ ≫ l = Cofork.π (c₁.map (F.flip.obj X₂)) ≫ 0 ≫ l

Tactic:
rwa [zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
i j : J
⊢ ∀ (f_1 : i ⟶ j),
    (Hom.hom ((G.obj (op i)).map f_1)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
      (Hom.hom ((G.map f_1.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)

Tactic:
g

Goal state after:
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
i j : J
g : i ⟶ j
⊢ (Hom.hom ((G.obj (op i)).map g)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
    (Hom.hom ((G.map g.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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 : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
⊢ (CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
      Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'' =
    G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫ (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom

Tactic:
by
    ext x
    dsimp
    simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]
    rw [← Functor.map_comp_assoc, ← right_coherence_app, Functor.map_comp_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
⊢ Φ.IsRightDerivabilityStructure

Tactic:
by
  have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
  have := Φ.isLocalizedEquivalence_of_functorial_right_resolutions i hi hW₁
  have := Φ.hasRightResolutions_arrow_of_functorial_resolutions i hi
  have := Φ.isConnected_rightResolution_of_functorial_resolutions i hi hW₁
  apply IsRightDerivabilityStructure.mk'

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : 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:
g

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f ≈ g → projectMapAux f✝ f = projectMapAux f✝ g
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 𝟙 (projectObj f✝¹ X✝) ≫ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝

Tactic:
Category.id_comp

Goal state after:
case id_comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f✝
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
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
⊢ ∀ (f : A' ⟶ A) (g : A ⟶ (sections I).obj X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
g

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
⊢ ∀ (g_1 : A ⟶ (sections I).obj X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (g ≫ g_1) =
      (toOver I).map g ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g_1
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
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
⊢ ∀ (g : X' ⟶ X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (u ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } u ≫ (sections I).map g

Tactic:
g

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (u ≫ g) =
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } u ≫ (sections I).map g