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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι

Tactic:
by
  ext
  simp [desc, descFOne, descFZero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f =
    pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)

Tactic:
Abelian.image.fac

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f = pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
Y✝ X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
k : KernelFork f
hk : IsLimit k
hf : W f
i : k.pt ≅ Y✝
⊢ W.kernels Y✝

Tactic:
exact .of_isLimit f (KernelFork.ofι (i.inv ≫ k.ι) (by simp))
      (IsLimit.ofIsoLimit hk (Fork.ext i)) hf

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
⊢ ∀ {X Y : C} (x : X ≅ Y), W.kernels X → W.kernels Y

Tactic:
by
    rintro _ _ i ⟨f, k, hk, hf⟩
    exact .of_isLimit f (KernelFork.ofι (i.inv ≫ k.ι) (by simp))
      (IsLimit.ofIsoLimit hk (Fork.ext i)) hf

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
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ((F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝¹))) x✝ =
    ((MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝¹))).comp (F.comp inl)) x✝

Tactic:
simp [inl_aut]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N K : Action V G
p : M.Hom N
q : N.Hom K
⊢ ∀ (g : G), M.ρ g ≫ p.hom ≫ q.hom = (p.hom ≫ q.hom) ≫ K.ρ g

Tactic:
intro g
    simp_all only [comm_assoc, comm, Category.assoc]

Goal state after:
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✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ } ⊗ F).map f ≫
      ε_ (F.obj Y)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj Y) =
    ε_ (F.obj X)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj X) ≫
      (𝟙_ (C ⥤ D)).map f

Tactic:
dsimp
            rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]

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

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

Tactic:
exact (inferInstance : Mono (((evaluation _ _).obj c).map η))

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

Goal state before:
pp: case mpr
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
adj : F ⋙ G ⊣ H ⋙ G := ⋯
⊢ IsIso t.adj₂.counit → IsIso t.adj₁.unit

Tactic:
intro h
    let adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
    exact t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
intro a b f g h η θ
    induction η using Quot.rec
    · induction θ using Quot.rec <;> rfl
    · rfl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ C a

Tactic:
have h₂ := (Part.mem_assert_iff.1 h).snd
  generalize_proofs at h₂
  clear h
  induction ‹Acc (Sum.inr · ∈ f ·) a› with | intro a ha IH => _
  have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩
  exact H a h fun a' fa' => IH a' fa' (Part.mem_assert_iff.1 (fix_fwd h fa')).snd

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ C a

Tactic:
by
  refine fixInduction h fun a' h ih => ?_
  rcases e : (f a').get (dom_of_mem_fix h) with b' | a'' <;> replace e : _ ∈ f a' := ⟨_, e⟩
  · apply hbase
    convert! e
    exact Part.mem_unique h (fix_stop e)
  · exact hind _ _ (fix_fwd h e) e (ih _ e)

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✝² : ∀ {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₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
⊢ g₁ ≫ Sigma.desc e = g₂ ≫ Sigma.desc e

Tactic:
apply_fun ((Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ ·) using
    (fun a b ↦ (cancel_epi _).mp)

Goal state after:
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✝² : ∀ {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₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
⊢ (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₁ ≫ Sigma.desc e) =
    (fun x ↦ (Sigma.desc fun a ↦ pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₂ ≫ Sigma.desc e)
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

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

Tactic:
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:
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
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
        (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
          (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)
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:
by
    intro a' g τ hτ
    use τ ≫ φ.inv
    refine ⟨?_, by cat_disch⟩
    simpa using (IsHomLift.comp p (g ≫ f) (isoOfIsoLift p f φ).inv τ φ.inv)

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
⊢ g * n * g⁻¹ ∈ MulAction.stabilizer (Aut F) x

Tactic:
rw [MulAction.mem_stabilizer_iff]

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
⊢ (g * n * g⁻¹) • x = x
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom (GrpCat.ofHom (autMapHom f.val))) ψ = φ

Tactic:
exact hψ

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}))
            ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).toEquiv
              (((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                    (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
                (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))))
        A).down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
erw [Types.limitEquivSections_apply, colimitCoyonedaHomIsoLimit'_π_apply]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ {
        down :=
          (ConcreteCategory.hom
              ((((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                        (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
                    (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f)).app
                ((incl F).obj A)))
            ((ConcreteCategory.hom ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A)).app ((incl F).obj A)))
              (𝟙 ((incl F).obj A))) }.down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
⊢ ∃ g, g • x = y

Tactic:
set x' : F'.obj X := (e X).symm x with hx'

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := (e X).symm x
hx' : x' = (e X).symm x
⊢ ∃ g, g • x = y
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
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).obj
⊢ ∃ g, ∀ (x : (F.obj X).obj), g • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F X
  obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G a (t.hom.app X a)
  exact ⟨g, action_ext_of_isGalois F _ hg⟩

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ EqvGen (HomRel.CompClosure redStep) (p ≫ Path.reverse p) (𝟙 X)

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 Y)

Tactic:
nth_rw 2 [← Quiver.Path.reverse_reverse p]

Goal state after:
V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ (Path.reverse p).reverse) =
    Quot.mk (HomRel.CompClosure redStep) (𝟙 Y)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ map F ⋙ lift G = lift (F ⋙ G)

Tactic:
apply lift_unique
  rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₃ + i₁ + i₂ = k

Tactic:
by rw [add_assoc, add_comm i₃, h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
h₁

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (g.f i) = Y.obj (g.f i)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
i : X.I
h₁ : f.f i = g.f i
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
h₁

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
i : X.I
h₁ : f.f i = g.f i
⊢ Y.obj (g.f i) = Y.obj (g.f i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ IsPushout 0 0 coprod.inl coprod.inr

Tactic:
by
  convert! @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
    <;> subsingleton

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

Goal state before:
pp: case zero
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n : ℕ
h : ¬0 < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) 0 ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < 0 + 1 then M i else N i) 0 ≫ eqToHom ⋯ ≫ f 0

Tactic:
have : n = 0 := by lia

Goal state after:
case zero
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n : ℕ
h : ¬0 < n
this : n = 0
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) 0 ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < 0 + 1 then M i else N i) 0 ≫ eqToHom ⋯ ≫ f 0
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)
s : Cocone (multispanIndexCoend F).multispan
⊢ ∀ (j : WalkingMultispan (multispanShapeCoend J)),
    (cowedge F).ι.app j ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ = s.ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).L
⊢ (cowedge F).ι.app (WalkingMultispan.left a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.left a✝)

case right
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a✝ : (multispanShapeCoend J).R
⊢ (cowedge F).ι.app (WalkingMultispan.right a✝) ≫ ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯ =
    s.ι.app (WalkingMultispan.right a✝)
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 : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
⊢ ∀ (j : WalkingMulticospan (multicospanShapeEnd J)),
    (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app j = s.π.app j

Tactic:
rintro (_ | _)

Goal state after:
case left
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).L
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.left a✝) =
    s.π.app (WalkingMulticospan.left a✝)

case right
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
a✝ : (multicospanShapeEnd J).R
⊢ (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩) ≫ (wedge F).π.app (WalkingMulticospan.right a✝) =
    s.π.app (WalkingMulticospan.right a✝)