mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : IsConnected X
⊢ IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X).obj

Tactic:
rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]
  exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X

Goal state after:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
hf : Finite ι
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)
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 : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
⊢ id t = id s

Tactic:
have h' : selfProdProj u t = selfProdProj u s := evaluation_injective_of_isConnected F A X b hs

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
h' : selfProdProj u t = selfProdProj u s
⊢ id t = id s
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 : 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

Tactic:
refine ⟨g, fun i y ↦ action_ext_of_isGalois F (x i) ?_ _⟩

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
i : ι
y : (F.obj (X i)).obj
⊢ g • x i = (ConcreteCategory.hom (t.hom.app (X i))) (x i)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this

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
| MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
      MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Z i₃)).hom (Y i₂) ≫
        (MonoidalCategoryStruct.associator (Z i₃) (X i₁) (Y i₂)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (Z i₃) (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) ≫
            ιTensorObj Z (tensorObj X Y) i₃ (i₁ + i₂) k ⋯ ≫ (associator Z X Y).inv k

Tactic:
← ιTensorObj₃_eq_assoc Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) _ rfl,

Goal state after:
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
| MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
      MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Z i₃)).hom (Y i₂) ≫
        (MonoidalCategoryStruct.associator (Z i₃) (X i₁) (Y i₂)).hom ≫
          ιTensorObj₃ Z X Y i₃ i₁ i₂ k ⋯ ≫ (associator Z X Y).inv k
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }

Tactic:
let hcⱼ := isLimitOfPreserves (Over.forget _ ⋙ (evaluation _ _).obj j) hc

Goal state after:
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
k : J
⊢ (s.fst ≫ (Over.Hom.left (α.app k)).app j) ≫ ({ diag := c, π := α, isLimit := hc }.diag.obj k).hom.app j =
    s.snd ≫ F.map f

Tactic:
by simp [← s.condition, ← NatTrans.comp_app]

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
⊢ ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f.op).app i ≫ coend.ι F i = (F.obj (op j)).map f ≫ coend.ι F j

Tactic:
by intros; apply coend.condition

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝¹ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, hf.incl.app b ≫ g₁ = hf.incl.app b ≫ g₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₁ =
    ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₂

Tactic:
simpa using! hj' _ hk

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: ⊢ ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
apply Finite.induction_empty_option

Goal state after:
case of_equiv
⊢ ∀ {α β : Type w} (a : α ≃ β),
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → C j ⥤ D j) (W : (j : α) → MorphismProperty (C j))
        [∀ (j : α), (W j).ContainsIdentities] [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi L).IsLocalization (MorphismProperty.pi W)) →
      ∀ {C : β → Type u₁} {D : β → Type u₂} [inst : (j : β) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : β) → Category.{v₂, u₂} (D j)] (L : (j : β) → C j ⥤ D j) (W : (j : β) → MorphismProperty (C j))
        [∀ (j : β), (W j).ContainsIdentities] [∀ (j : β), (L j).IsLocalization (W j)],
        (Functor.pi L).IsLocalization (MorphismProperty.pi W)

case h_empty
⊢ ∀ {C : PEmpty.{w + 1} → Type u₁} {D : PEmpty.{w + 1} → Type u₂}
    [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

case h_option
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → C j ⥤ D j) (W : (j : α) → MorphismProperty (C j))
        [∀ (j : α), (W j).ContainsIdentities] [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi L).IsLocalization (MorphismProperty.pi W)) →
      ∀ {C : Option α → Type u₁} {D : Option α → Type u₂} [inst : (j : Option α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : Option α) → Category.{v₂, u₂} (D j)] (L : (j : Option α) → C j ⥤ D j)
        (W : (j : Option α) → MorphismProperty (C j)) [∀ (j : Option α), (W j).ContainsIdentities]
        [∀ (j : Option α), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.LocallySmall

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
this✝¹ : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : C ⥤ InducedCategory D L.obj :=
  { obj := fun X ↦ X, map := fun {X Y} f ↦ InducedCategory.homMk (L.map f), map_id := ⋯, map_comp := ⋯ }
this✝ : L.EssSurj
this : (inducedFunctor L.obj).EssSurj
⊢ W.HasLocalization

Tactic:
(Tactic.tacticHave__
 "have"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId (hygieneInfo `[anonymous]))
   []
   [(Term.typeSpec
     ":"
     (Term.proj
      (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `inducedFunctor [`L.obj]) ")")
      "."
      `IsEquivalence))]
   ":="
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))))

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
this✝² : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : C ⥤ InducedCategory D L.obj :=
  { obj := fun X ↦ X, map := fun {X Y} f ↦ InducedCategory.homMk (L.map f), map_id := ⋯, map_comp := ⋯ }
this✝¹ : L.EssSurj
this✝ : (inducedFunctor L.obj).EssSurj
this : (inducedFunctor L.obj).IsEquivalence
⊢ W.HasLocalization
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
⊢ ∀ {C : PEmpty.{w + 1} → Type u₁} {D : PEmpty.{w + 1} → Type u₂}
    [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
intro C D _ _ L W _ _
    have : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
    refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)
    rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
    rintro ⟨⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hᵣ
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd

Tactic:
· exact congrArg (fun t ↦ t.app x) e₂

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun x ↦ (ConcreteCategory.hom (f ≫ g).of) x) =
    (fun x ↦ (ConcreteCategory.hom f.of) x) ≫ fun x ↦ (ConcreteCategory.hom g.of) x

Tactic:
by
        dsimp
        ext t
        simp [joinM]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (αₗ x y z).hom ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f) ≫ (αₗ x y z').inv

Tactic:
rw [← Category.assoc, ← actionAssocIso_hom_naturality]

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ (αₗ x y z').hom) ≫ (αₗ x y z').inv
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = (αᵣ z x y).hom ≫ ((f ⊙ᵣₘ 𝟙 x) ⊙ᵣₘ 𝟙 y) ≫ (αᵣ z' x y).inv

Tactic:
rw [← Category.assoc, ← actionAssocIso_hom_naturality]

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ (αᵣ z' x y).hom) ≫ (αᵣ z' x y).inv
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷ c.pt ≫
      hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } =
    (α_ c.pt c.pt c.pt).hom ≫
      c.pt ◁ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ≫
        hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }

Tactic:
apply hc.hom_ext
    simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsLimit.fac,
      mon_tauto, implies_true]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = 𝟙_ C ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X

Tactic:
actionHom_def',

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = 𝟙_ C ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X

Tactic:
actionHom_def',

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ μ ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ yoneda.obj (G ⊗ H) ⟶ yoneda.obj H

pp: case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Yoneda.fullyFaithful.preimage ?refine_2.refine_1 ≫ φ = G ◁ φ ≫ conj G

Tactic:
· refine ⟨fun X ↦ ↾fun x ↦ h' _ (x ≫ fst _ _) (x ≫ snd _ _), fun X Y f ↦ ?_⟩
      ext
      simp [← cancel_mono φ, hh', comp_mul, comp_inv]

Goal state after:
case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Yoneda.fullyFaithful.preimage
        { app := fun X ↦ ↾fun x ↦ h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H), naturality := ⋯ } ≫
      φ =
    G ◁ φ ≫ conj G