mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.LeftInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ Function.RightInverse (fun f ↦ ⇑(ConcreteCategory.hom f)) fun f ↦ ↾f

Tactic:
intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g : G
x : G ⧸ N
⊢ (ConcreteCategory.hom
        ((ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯)))
      x =
    (ConcreteCategory.hom
        (FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g))
      x

Tactic:
induction x using Quotient.inductionOn with | h x
       =>  _ 

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g x : G
⊢ (ConcreteCategory.hom
        ((ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯)))
      ⟦x⟧ =
    (ConcreteCategory.hom
        (FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g))
      ⟦x⟧
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
F : N ⋊[φ] G →* H
⊢ F = lift (F.comp inl) (F.comp inr) ⋯

Tactic:
rw [DFunLike.ext_iff]

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
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
G : D ⥤ₑ E
e : (whiskeringLeft L P E).obj G ≅ F
⊢ P.isoModSerre.IsInvertedBy F.obj

Tactic:
rw [← MorphismProperty.IsInvertedBy.iff_of_iso _
      (show L ⋙ G.obj ≅ F.obj from (ObjectProperty.ι _).mapIso e)]

Goal state after:
case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
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
G : D ⥤ₑ E
e : (whiskeringLeft L P E).obj G ≅ F
⊢ P.isoModSerre.IsInvertedBy (L ⋙ G.obj)
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), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ({ obj := fun t ↦ ∐ fun x ↦ x✝, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f), map_id := ⋯,
              map_comp := ⋯ }.map
          f_1 ≫
        Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
      (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫
        { obj := fun t ↦ ∐ fun x ↦ d₂, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f),
              map_id := ⋯, map_comp := ⋯ }.map
          f_1

Tactic:
by
        intros
        dsimp
        ext
        simp

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

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : F.FullyFaithful
this✝ : F.Full
this : F.Faithful
⊢ IsIso t.adj₂.counit

Tactic:
rw [← t.isIso_unit_iff_isIso_counit]
      infer_instance

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

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op t.leftToRight).app x✝

Tactic:
leftToRight_eq_counits

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x✝
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
rw [naturality_id]
      bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
rw [naturality_id]
      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
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom

Tactic:
mapComp'

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp f (𝟙 b₁)).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom
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
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom

Tactic:
mapComp'

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp (𝟙 b₀) f).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
j : I
X Y✝ : C j
f : X ⟶ Y✝
⊢ (F.map (SigmaHom.mk f) ≫
      match ⟨j, Y✝⟩ with
      | ⟨j, X⟩ => (h j).app X) =
    (match ⟨j, X⟩ with
      | ⟨j, X⟩ => (h j).app X) ≫
      G.map (SigmaHom.mk f)

Tactic:
apply (h j).naturality

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := { toFun := Option.map (f ≫ g).toFun, map_fst := ⋯, map_snd := ⋯ } } =
    { hom := { toFun := Option.map f.toFun, map_fst := ⋯, map_snd := ⋯ } } ≫
      { hom := { toFun := Option.map g.toFun, map_fst := ⋯, map_snd := ⋯ } }

Tactic:
ext : 3
    exact (Option.map_comp_map f.1 g.1).symm

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

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

Tactic:
simp only [Category.assoc, Hom.mk.injEq, true_and]
    rw [← Category.assoc, ← Category.assoc]; congr 1
    ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫ EffectiveEpi.desc (Sigma.desc π) (Sigma.desc e) ⋯ = e a

Tactic:
by
    rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]

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✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
⊢ ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f) =
    (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ (((diagram V F₁ F₂).obj (Opposite.op i)).obj i)).inv ▷ ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
        (((diagram V F₁ F₂).obj (Opposite.op i)).obj i ◁ (eHomEquiv V) (F₂.map f)) ▷
            ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (F₂.obj j) ▷
              ((diagram V F₂ F₃).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j) (F₃.obj j)

Tactic:
have := end_.condition (diagram V F₂ F₃) f
      dsimp [eHomWhiskerLeft, eHomWhiskerRight] at this ⊢
      conv_lhs => rw [assoc, tensorHom_def_assoc]
      conv_rhs =>
        rw [tensorHom_def_assoc, whisker_assoc_assoc, e_assoc,
          triangle_assoc_comp_right_inv_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          assoc, assoc, ← this, MonoidalCategory.whiskerLeft_comp_assoc,
          MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
          ← e_assoc, whiskerLeft_rightUnitor_inv_assoc, associator_inv_naturality_right_assoc,
          Iso.hom_inv_id_assoc, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc,
          Iso.inv_hom_id_assoc]

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 : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ inferInstance)

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

Goal state before:
pp: 𝒮 : 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 : a'.base ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
inst✝ : (forget F).IsHomLift (g ≫ f) φ'
⊢ φ'.base = g ≫ f

Tactic:
by simpa using IsHomLift.fac' (forget F) (g ≫ f) φ'

Goal state after:
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
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
m : s.pt ⟶ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).pt
hm : ∀ (j : StructuredArrow (L.obj Y) L), m ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app j = s.π.app j
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y

Tactic:
have := hm (StructuredArrow.mk (𝟙 (L.obj Y)))

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
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
m : s.pt ⟶ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).pt
hm : ∀ (j : StructuredArrow (L.obj Y) L), m ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app j = s.π.app j
this :
  m ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (𝟙 (L.obj Y))) =
    s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y
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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.fst f g))) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

Tactic:
simp only [fiberPullbackEquiv, Functor.comp_map, Iso.toEquiv_symm_fun]
  change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫
    (F ⋙ FintypeCat.incl).map (pullback.fst f g)) _ = _
  erw [PreservesPullback.iso_inv_fst, Types.pullbackIsoPullback_inv_fst]
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A X : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Finite (A ⟶ X)

Tactic:
apply Finite.of_injective (fun f ↦ F.map f a)

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

Goal state before:
pp: case pos
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 }
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
have hn1 : Nat.card (F.obj Y) < n := by
      rw [hn]
      exact lt_card_fiber_of_mono_of_notIso F v hvnoiso

Goal state after:
case pos
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
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
m : ↥V ⧸ (↑U).subgroupOf ↑V
x : Aut F ⧸ ↑U
⊢ (ConcreteCategory.hom
        (u.inv ≫
            (functorToAction F).map ((quotientDiag V h u).map m) ≫ u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV).hom)
      x =
    (ConcreteCategory.hom (quotientToQuotientOfLE (↑V) (↑U) hUinV).hom) x

Tactic:
induction m, x using Quotient.inductionOn₂ with | _ σ μ
     =>  _ 

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ (ConcreteCategory.hom
        (u.inv ≫
            (functorToAction F).map ((quotientDiag V h u).map ⟦σ⟧) ≫
              u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV).hom)
      ⟦μ⟧ =
    (ConcreteCategory.hom (quotientToQuotientOfLE (↑V) (↑U) hUinV).hom) ⟦μ⟧
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
hpx : ∀ (i : ι), (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i
A : C
f : A ⟶ P
a : (F.obj A).obj
left✝ : IsGalois A
hfa : (ConcreteCategory.hom (F.map f)) a = px
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
obtain ⟨g, hg⟩ := toAut_surjective_isGalois F G t A

Goal state after:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
hpx : ∀ (i : ι), (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i
A : C
f : A ⟶ P
a : (F.obj A).obj
left✝ : IsGalois A
hfa : (ConcreteCategory.hom (F.map f)) a = px
g : G
hg : ∀ (x : (F.obj A).obj), g • x = (ConcreteCategory.hom (t.hom.app A)) x
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {p | Discrete.Arrows c d p} →
      ∀ {q : d ⟶ e}, q ∈ {p | Discrete.Arrows d e p} → p ≫ q ∈ {p | Discrete.Arrows c e p}

Tactic:
rintro _ _ _ _ ⟨⟩ _ ⟨⟩; rw [Category.comp_id]; constructor

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
⊢ f ∈ (im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
convert! Map.arrows_iff φ hφ ⊤ f

Goal state after:
case e'_2
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c d : D
f : c ⟶ d
x✝⁴ x✝³ : C
x✝² : x✝⁴ ⟶ x✝³
x✝¹ : φ.obj x✝⁴ = c
x✝ : φ.obj x✝³ = d
⊢ f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝ ↔ ∃ (_ : x✝² ∈ ⊤.arrows x✝⁴ x✝³), f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝
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
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ : ∃ a b g, ∃ (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
obtain ⟨c, c', γ, cd, cd', γS, hγ⟩ := hδ

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
d d' : D
g : d ⟶ d'
δ : d ⟶ d
c c' : C
γ : c ⟶ c'
cd : φ.obj c = d
cd' : φ.obj c' = d
γS : γ ∈ S.arrows c c'
hγ : δ = eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd'
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : r • (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
← map_smul (colimit.ι F j).hom

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
s : Cone (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F)
x : (coyoneda.obj (op j)).Elements
⊢ WeightedCone.π s (𝟙 j) ≫ (WeightedCone.coyoneda F j).π.app x = s.π.app x

Tactic:
by
    simpa using s.w (CategoryOfElements.homMk (Functor.elementsMk _ j (𝟙 j)) x x.snd (by simp))

Goal state after: