mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ a'.hom ≫ g = 0

Tactic:
apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := ⋯
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ p' ≫ a'.hom ≫ g = 0
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 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map (z ≫ f) = 0
⊢ L.map z = 0

Tactic:
rw [map_eq_zero_iff L P, ← exists_comp_monoModSerre_eq_zero_iff P] at hz ⊢

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 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : ∃ Y' s, ∃ (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), z ≫ s = 0
Module: Mathlib.CategoryTheory.Action.Concrete

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

Tactic:
change ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ x : G
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj Y)
        (F.obj Y) =
    η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj X)
        (F.obj X) ≫
      ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ } ⊗ F).map f

Tactic:
simp [tensorHom_def, coevaluation_comp_leftAdjointMate_assoc]

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
⊢ (whiskeringLeft L P E).essImage F ↔ P.isoModSerre.IsInvertedBy F.obj

Tactic:
refine ⟨?_, fun hF ↦ ?_⟩

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
⊢ (whiskeringLeft L P E).essImage F → P.isoModSerre.IsInvertedBy F.obj

case refine_2
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ (whiskeringLeft L P E).essImage F
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
g : G
f : Fin n → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
induction n generalizing g with
  | zero =>
    funext (x : Fin 1)
    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]
  | succ n hn =>
    funext x
    induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using! congrFun (hn (g * f 0) (Fin.tail f)) i

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)

Tactic:
by
  constructor
  · intro h c
    exact (inferInstance : Epi (((evaluation _ _).obj c).map η))
  · intros
    apply NatTrans.epi_of_epi_app

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

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

Tactic:
by
    simp [-LeftExtension.w, ← LeftExtension.w η]

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) ⊗≫ τ
⊢ t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv

Tactic:
by
          rw [Hσ]
          dsimp only [τ]
          bicategory

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ b ∈
    match e : (f a).get h₁ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      (fun y p ↦
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            y ⋯)
        a' ⋯

Tactic:
split

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

case h_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
a'✝ : α
heq✝ : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p ↦
        WellFounded.fixF
          (fun a IH ↦
            Part.assert (f a).Dom fun hf ↦
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Dom ∪ f.Domᶜ)

Tactic:
Set.union_comm (Dom f),

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = (f.core s ∪ f.Domᶜ) ∩ (f.Domᶜ ∪ f.Dom)
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 ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom =
    (mapPullbackAdj (𝟙 X)).unit

Tactic:
Adjunction.unit_rightAdjointUniq_hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
⊢ (mapPullbackAdj (𝟙 X)).unit = (mapPullbackAdj (𝟙 X)).unit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ (mapPullbackAdj (f ≫ g)).unit ≫
      (map (f ≫ g)).whiskerLeft ((mapPullbackAdj (f ≫ g)).rightAdjointUniq (mapPullbackAdj (f ≫ g))).hom =
    (mapPullbackAdj (f ≫ g)).unit

Tactic:
Adjunction.unit_rightAdjointUniq_hom

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ (mapPullbackAdj (f ≫ g)).unit = (mapPullbackAdj (f ≫ g)).unit
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
⊢ W.IsInvertedBy₂ W (curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj L')

Tactic:
rintro ⟨X₁, Y₁⟩ ⟨X₂, Y₂⟩ ⟨f₁, f₂⟩ ⟨hf₁, hf₂⟩
  have := Localization.inverts L' W _ (W.whiskerRight_mem f₁ hf₁ Y₁)
  have := Localization.inverts L' W _ (W.whiskerLeft_mem X₂ f₂ hf₂)
  dsimp
  infer_instance

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

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (F'.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (F'.map φ.op).app j'

Tactic:
have e := (f.app (op j)).naturality φ
    simp only [Category.assoc]
    rw [← e, reassoc_of% end_.condition F φ]
    simp

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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₁, ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y₁) := ⟨_, ⟨(L').objObjPreimageIso Y₁⟩⟩
  obtain ⟨X₂, ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y₂) := ⟨_, ⟨(L').objObjPreimageIso Y₂⟩⟩
  obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩
  obtain ⟨X₄, ⟨e₄⟩⟩ : ∃ X₄, Nonempty ((L').obj X₄ ≅ Y₄) := ⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩
  suffices Pentagon ((L').obj X₁) ((L').obj X₂) ((L').obj X₃) ((L').obj X₄) by
    dsimp [Pentagon]
    refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
    · rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]
    · rw [assoc, associator_naturality_assoc, associator_naturality_assoc,
        ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, ← tensor_comp,
        e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id, comp_id]
  dsimp [Pentagon]
  have : ((L').obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ (L').obj X₄ ≫
      (α_ ((L').obj X₁) ((L').obj X₂ ⊗ (L').obj X₃) ((L').obj X₄)).hom ≫
        (L').obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ (L').obj X₄ =
          (α_ ((L').obj X₁) ((L').obj (X₂ ⊗ X₃)) ((L').obj X₄)).hom :=
    pentagon_aux₂ _ _ _ (μ L W ε X₂ X₃).symm
  rw [associator_hom_app, tensorHom_id, id_tensorHom, associator_hom_app, tensorHom_id,
    whiskerLeft_comp, whiskerRight_comp, whiskerRight_comp, whiskerRight_comp, assoc, assoc,
    assoc, whiskerRight_comp, assoc,
    reassoc_of% this, associator_hom_app, tensorHom_id,
    ← pentagon_aux₁ (X₂ := (L').obj X₃) (X₃ := (L').obj X₄) (i := μ L W ε X₁ X₂),
    ← pentagon_aux₃ (X₁ := (L').obj X₁) (X₂ := (L').obj X₂) (i := μ L W ε X₃ X₄),
    associator_hom_app, associator_hom_app]
  simp only [assoc, ← whiskerRight_comp_assoc, Iso.inv_hom_id, comp_id, μ_natural_left_assoc,
    id_tensorHom, ← whiskerLeft_comp, Iso.inv_hom_id_assoc]
  rw [← (L').map_comp_assoc, whiskerLeft_comp, μ_inv_natural_right_assoc, ← (L').map_comp_assoc]
  simp only [assoc, MonoidalCategory.pentagon, Functor.map_comp, tensorHom_id,
    whiskerRight_comp_assoc]
  congr 3; simp only [← assoc]; congr
  simp only [← cancel_mono (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv, assoc, id_comp,
    whisker_exchange_assoc, ← whiskerRight_comp_assoc,
    Iso.inv_hom_id, whiskerRight_id, ← whiskerLeft_comp,
    whiskerLeft_id]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝

Tactic:
ext c
      simp [symm, symmEquivInverse]

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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)

Tactic:
apply of_commSq

Goal state after:
case h
𝒮 : 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.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ?ha) (eqToHom ?hb) (f ≫ g)

case ha
𝒮 : 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.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj a = R

case hb
𝒮 : 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.IsHomLift f φ
inst✝ : p.IsHomLift g ψ
⊢ p.obj c = T
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.IsCartesian f φ
a' : 𝒳
φ' : a' ⟶ b
inst✝ : p.IsCartesian f φ'
⊢ IsCartesian.map p f φ φ' ≫ IsCartesian.map p f φ' φ = 𝟙 a'

Tactic:
subst_hom_lift p f φ'
    apply IsCartesian.ext p (p.map φ') φ'
    simp only [assoc, fac, id_comp]

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.hom φ.hom
⊢ p.IsHomLift f.inv φ.inv

Tactic:
apply of_commSq

Goal state after:
case h
𝒮 : 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 φ.hom
⊢ CommSq (p.map φ.inv) (eqToHom ?ha) (eqToHom ?hb) f.inv

case ha
𝒮 : 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 φ.hom
⊢ p.obj b = S

case hb
𝒮 : 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 φ.hom
⊢ p.obj a = R
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 φ.hom
⊢ p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv

Tactic:
apply of_commSq

Goal state after:
case h
𝒮 : 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
⊢ CommSq (p.map φ.inv) (eqToHom ?ha) (eqToHom ?hb) (isoOfIsoLift p f φ).inv

case ha
𝒮 : 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
⊢ p.obj b = S

case hb
𝒮 : 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
⊢ p.obj a = R
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c } =
    { base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
      { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }

Tactic:
by
    ext
    · simp
    · simp [← (F.mapId ⟨op S⟩).inv.toNatTrans.naturality_assoc ψ, F.whiskerRight_mapId_inv_app,
        Strict.leftUnitor_eqToIso, ← Cat.Hom₂.comp_app]

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
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
⊢ Nat.card (F.obj Z).obj < n

Tactic:
hn,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
⊢ Nat.card (F.obj Z).obj < Nat.card (F.obj X).obj
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
t : (F.obj X).obj
⊢ (ConcreteCategory.hom ((piComparison F fun x ↦ X) ≫ Pi.π (fun b ↦ F.obj X) t)) (mkSelfProdFib F X) = t

Tactic:
simp [← PreservesProduct.iso_hom, mkSelfProdFib]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ ((FintypeCat.uSwitchEquivalence.functor.mapAction (Aut F')).obj X.obj).IsContinuous

Tactic:
by
          rw [Action.isContinuous_def]
          change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
          exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop))

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ ((FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F')).obj X.obj).IsContinuous

Tactic:
by
          rw [Action.isContinuous_def]
          change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
          exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop))

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ S ∈ 𝓝 1 ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

Tactic:
mem_nhds_iff

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S