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

Goal state before:
pp: case min.refine_1
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⟩)
⊢ CofilteredClosureSmall.InductiveStep (max n m + 1) fun m_1 x ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure f m_1

Tactic:
refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y

Goal state after:
case min.refine_1.refine_1
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⟩)
⊢ n < max n m + 1

case min.refine_1.refine_2
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⟩)
⊢ m < max n m + 1
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
inst✝ : Φ.IsIdempotent
X : C
⊢ IsIso (Φ.r.map (Φ.ι.app X))

Tactic:
by
  rw [r_map_ι_app]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) (n✝ + 1)

Tactic:
rw [quasiIsoAt_iff_exactAt]
      · apply ofCocomplex_exactAt_succ
      · apply CochainComplex.exactAt_succ_single_obj

Goal state after:
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ X' t, ∃ (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂

Tactic:
refine ⟨_, kernel.ι (f₁ - f₂), ?_, ?_⟩
    · rw [isoModSerre_iff_of_mono]
      exact P.prop_of_iso (Abelian.coimageIsoImage (f₁ - f₂)).symm
        ((exists_comp_isoModSerre_eq_zero_iff P _).1 ⟨_ ,s, hs, by simpa [sub_eq_zero]⟩)
    · simpa only [Preadditive.comp_sub, sub_eq_zero] using kernel.condition (f₁ - f₂)

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ∀ (x y : G),
    ⟨fun b ↦ F.map (homOfPair b (x * y)), x * y⟩ =
      ⟨fun b ↦ F.map (homOfPair b x), x⟩ * ⟨fun b ↦ F.map (homOfPair b y), y⟩

Tactic:
by
      intro g h
      ext b
      · exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
      rfl

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
n : N
⊢ (lift fn fg h) (inl n) = fn n

Tactic:
simp [lift]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
g : G
⊢ (lift fn fg h) (inr g) = fg g

Tactic:
simp [lift]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ (eqToHomTransIso e₁ ⋯).hom = (ρ_ (eqToHom e₁)).symm.hom

Tactic:
subst e₁

Goal state after:
B : Type u
inst✝ : Bicategory B
x : B
⊢ (eqToHomTransIso ⋯ ⋯).hom = (ρ_ (eqToHom ⋯)).symm.hom
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ (eqToHomTransIso ⋯ e₁).hom = (λ_ (eqToHom e₁)).symm.hom

Tactic:
subst e₁

Goal state after:
B : Type u
inst✝ : Bicategory B
x : B
⊢ (eqToHomTransIso ⋯ ⋯).hom = (λ_ (eqToHom ⋯)).symm.hom
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).hom =
    (eqToHomTransIso e₁ e₂).inv ▷ eqToHom e₃ ≫
      (eqToHomTransIso ⋯ e₃).inv ≫ (eqToHomTransIso e₁ ⋯).hom ≫ eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).hom

Tactic:
subst_vars

Goal state after:
B : Type u
inst✝ : Bicategory B
t : B
⊢ (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)).hom =
    (eqToHomTransIso ⋯ ⋯).inv ▷ eqToHom ⋯ ≫
      (eqToHomTransIso ⋯ ⋯).inv ≫ (eqToHomTransIso ⋯ ⋯).hom ≫ eqToHom ⋯ ◁ (eqToHomTransIso ⋯ ⋯).hom
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
e₁ : x = y
e₂ : y = z
e₃ : z = t
⊢ (α_ (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).inv =
    eqToHom e₁ ◁ (eqToHomTransIso e₂ e₃).inv ≫
      (eqToHomTransIso e₁ ⋯).inv ≫ (eqToHomTransIso ⋯ e₃).hom ≫ (eqToHomTransIso e₁ e₂).hom ▷ eqToHom e₃

Tactic:
subst_vars

Goal state after:
B : Type u
inst✝ : Bicategory B
t : B
⊢ (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)).inv =
    eqToHom ⋯ ◁ (eqToHomTransIso ⋯ ⋯).inv ≫
      (eqToHomTransIso ⋯ ⋯).inv ≫ (eqToHomTransIso ⋯ ⋯).hom ≫ (eqToHomTransIso ⋯ ⋯).hom ▷ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (α_ f g h).hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯

Tactic:
subst_vars

Goal state after:
B : Type u
inst✝ : Bicategory B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f f' : x ⟶ y
g g' : y ⟶ z
h h' : z ⟶ t
ef : f = f'
eg : g = g'
eh : h = h'
⊢ (α_ f g h).inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯

Tactic:
subst_vars

Goal state after:
B : Type u
inst✝ : Bicategory B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X✝ Y✝ : LeftLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f = h ◁ Y✝.unit ≫ (α_ h Y✝.lift f).inv

Tactic:
rw [← LeftLift.w η]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X✝ Y✝ : LeftLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f =
    h ◁ (X✝.unit ≫ StructuredArrow.Hom.right η ▷ f) ≫ (α_ h Y✝.lift f).inv
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} J✝
J : Type ?u.6
inst✝ : Category.{v_1, ?u.6} J
X : Type u_1
f : ConnectedComponents J → X
x : ConnectedComponents J
⊢ liftFunctor J (functorToDiscrete X f) x = f x

Tactic:
obtain ⟨x, h⟩ := Quotient.exists_rep x
    rw [← h]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ ∀ {X Y : Decomposed J}, Function.Surjective (decomposedTo J).map

Tactic:
rintro ⟨j', X, hX⟩ ⟨k', Y, hY⟩ f

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : (decomposedTo J).obj ⟨j', { obj := X, property := hX }⟩ ⟶ (decomposedTo J).obj ⟨k', { obj := Y, property := hY }⟩
⊢ ∃ a, (decomposedTo J).map a = f
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ f.fix a = f.fix a'

Tactic:
ext b; constructor
  · intro h
    obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'
    exact e'
  · intro h
    rw [PFun.mem_fix_iff]
    exact Or.inr ⟨a', ha', h⟩

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ f.fn ↑x ⋯ ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x

Tactic:
exact
    Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
      have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
      Part.mem_unique fxy this ▸ ys

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾g ≫ ↾f = 𝟙 Y

Tactic:
ext y

Goal state after:
case h.right
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
y : Y
⊢ (ConcreteCategory.hom (↾g ≫ ↾f)).toFun y = (ConcreteCategory.hom (𝟙 Y)).toFun y
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (fun f ↦ { hom := { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
      ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
by
            ext (_ | _) : 4
            · exact f.hom.map_fst.symm
            · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
⊢ (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯) =
    𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y)

Tactic:
ext f

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f : (hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y
⊢ (hom (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯)).toFun f =
    (hom (𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y))).toFun f
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

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

Tactic:
by
  rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
⊢ lift a b h ≫ snd f g = b

Tactic:
simp [lift]

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
f₂ : X₂ ⟶ Y₂
⊢ (X₁ ◁ f₂) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ f₂ ▷ X₃

Tactic:
by
  simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom ≫ L'.map (X' ◁ (λ_ Y').hom) =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map ((ρ_ X').hom ▷ Y')
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
← μ_natural_left,

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom ≫ L'.map (X' ◁ (λ_ Y').hom) =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ L'.map (ρ_ X').hom ▷ L'.obj Y' ≫ (μ L W ε X' Y').hom
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
⊢ f = g

Tactic:
ext y

Goal state after:
case fst
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).1 = (↑((ConcreteCategory.hom g).toFun y)).1

case snd
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).2 = (↑((ConcreteCategory.hom g).toFun y)).2
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

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 φ
a' : 𝒳
h : a' = a
⊢ p.IsHomLift f (eqToHom h ≫ φ)

Tactic:
subst h; simp_all

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 : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
b' : 𝒳
h : b = b'
⊢ p.IsHomLift f (φ ≫ eqToHom h)

Tactic:
subst h; simp_all

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 : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
R' : 𝒮
h : R' = R
⊢ p.IsHomLift (eqToHom h ≫ f) φ

Tactic:
subst h; simp_all

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 : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
S' : 𝒮
h : S = S'
⊢ p.IsHomLift (f ≫ eqToHom h) φ

Tactic:
subst h; simp_all

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.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst✝ : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ' φ ≫ IsCocartesian.map p f φ φ' = 𝟙 b'

Tactic:
by
    subst_hom_lift p f φ'
    apply IsCocartesian.ext p (p.map φ') φ'
    simp only [fac_assoc, fac, comp_id]

Goal state after:
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'
⊢ 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 ≫
      (functorEnrichedHom V F₁ F₂).map f ≫
        enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) ≫
          eHomWhiskerRight V (F₁.map f) (F₂.obj j')

Tactic:
simp only [functorEnrichedHom_obj, functorEnrichedHom_map, end_.lift_π_assoc, diagram_obj_obj,
      Functor.comp_obj, Under.forget_obj, Under.mk_right, Under.map_obj_right, Iso.refl_inv,
      NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id]

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'
⊢ 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')
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
⊢ Nat.card (A ⟶ X) ≤ Nat.card (F.obj X).obj

Tactic:
apply Nat.card_le_card_of_injective

Goal state after:
case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ Function.Injective ?f

case f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ (A ⟶ X) → (F.obj X).obj
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 : C
inst✝ : IsConnected A
a : (F.obj A).obj
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).obj

Tactic:
apply Nat.card_le_card_of_injective

Goal state after:
case hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).obj
⊢ Function.Injective ?f

case f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).obj
⊢ Aut A → (F.obj A).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ (∀ (i : Empty), IsConnected ((fun x ↦ X) i)) ∧ Finite Empty

Tactic:
exact ⟨by simp only [IsEmpty.forall_iff], inferInstance⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : (ConcreteCategory.hom (F.map φ.hom)) x = g⁻¹ • x
⊢ g • n • (ConcreteCategory.hom (F.map φ.hom)) x = x

Tactic:
mulAction_naturality,

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).obj
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : (ConcreteCategory.hom (F.map φ.hom)) x = g⁻¹ • x
⊢ g • (ConcreteCategory.hom (F.map φ.hom)) (n • x) = x
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := ⋯
a a' : (F.obj A).obj
ha' : (ConcreteCategory.hom (F.map f)) a' = (ConcreteCategory.hom (F.map σ.hom)) ((ConcreteCategory.hom (F.map f)) a)
τ : Aut A
hτ : (ConcreteCategory.hom (F.map τ.hom)) a = a'
⊢ (fun f_1 ↦ (ConcreteCategory.hom (F.map f_1.hom)) ((ConcreteCategory.hom (F.map f)) a)) (autMap f τ) =
    (fun f_1 ↦ (ConcreteCategory.hom (F.map f_1.hom)) ((ConcreteCategory.hom (F.map f)) a)) σ

Tactic:
simp [hτ, ha']

Goal state after:
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 A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
have : IsIso u := IsConnected.noTrivialComponent Y u hn

Goal state after:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this : IsIso u
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b