mathlib-initiative/mathlib-tactics huggingface dataset:
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
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha✝ : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
x : (F.obj X).obj
j : fι ⟨X, XinI⟩
a : ((Discrete.functor (ff ⟨X, XinI⟩) ⋙ F).obj { as := j }).obj
ha : (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a = x
⊢ (ConcreteCategory.hom (σ.hom.app X)) x = x

Tactic:
← ha,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha✝ : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
x : (F.obj X).obj
j : fι ⟨X, XinI⟩
a : ((Discrete.functor (ff ⟨X, XinI⟩) ⋙ F).obj { as := j }).obj
ha : (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a = x
⊢ (ConcreteCategory.hom (σ.hom.app X))
      ((ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a) =
    (ConcreteCategory.hom (F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }))) a
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
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ σ • x = y

Tactic:
← ha,

Goal state after:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ σ • (ConcreteCategory.hom (F.map f)) a = y
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
let (i : ι) : TopologicalSpace (f i).V := ⊥

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case h
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ (gi X)⁻¹ • gi X • X.pt = X.pt

Tactic:
inv_smul_smul

Goal state after:
case h
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ X.pt = X.pt
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
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G

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

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c : C
⊢ c ∈ ⊤.objs

Tactic:
dsimp [Top.top, objs]

Goal state after:
C : Type u
inst✝ : Groupoid C
c : C
⊢ univ.Nonempty
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Groupoid C
S✝ : Subgroupoid C
s : Set (Subgroupoid C)
S : Subgroupoid C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ F ∈ sInf s → F ∈ S

Tactic:
simp only [mem_sInf]

Goal state after:
case refine_1
C : Type u
inst✝ : Groupoid C
S✝ : Subgroupoid C
s : Set (Subgroupoid C)
S : Subgroupoid C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ (∀ S ∈ s, F ∈ S) → F ∈ S
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
T : Subgroupoid C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ F ∈ sInf s

Tactic:
simp only [mem_sInf]

Goal state after:
case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
T : Subgroupoid C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ ∀ S ∈ s, F ∈ S
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.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
      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.tensorHom (𝟙 (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:
Iso.inv_hom_id_assoc,

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 ≫
          MonoidalCategoryStruct.tensorHom (𝟙 (Z i₃)) (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) ≫
            ιTensorObj Z (tensorObj X Y) i₃ (i₁ + i₂) k ⋯ ≫ (associator Z X Y).inv k
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d✝ d✝

Tactic:
convert! Sn.conj (Groupoid.inv p) hs

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p = Groupoid.inv (Groupoid.inv p)
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: case left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).L
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ g

Tactic:
simpa using! _ ≫= h _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a b c d : C ⋆ D
f : a.Hom b
g : b.Hom c
h : c.Hom d
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases a <;>
    cases b

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : C
g : (left a✝).Hom c
f : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ : C
a✝ : D
g : (right a✝).Hom c
f : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ : D
a✝ : C
g : (left a✝).Hom c
f : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
c d : C ⋆ D
h : c.Hom d
a✝¹ a✝ : D
g : (right a✝).Hom c
f : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom
          ((monoFactorisation f).I.map g ≫
            ↾fun x ↦
              match x with
              | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx))).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
            H.I.map g)).toFun
      x✝

Tactic:
apply injective_of_mono (H.m.app Y)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom (H.m.app Y))
      ((ConcreteCategory.hom
            ((monoFactorisation f).I.map g ≫
              ↾fun x ↦
                match x with
                | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx))).toFun
        x✝) =
    (ConcreteCategory.hom (H.m.app Y))
      ((ConcreteCategory.hom
            ((↾fun x ↦
                match x with
                | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
              H.I.map g)).toFun
        x✝)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
hm : { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a = s.proj a
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a

Tactic:
rw [hom_ext_iff] at hm

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
hm :
  ∃ (h₁ : ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).f = (s.proj a).f),
    ∀ (i : s.pt.I), ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).φ i ≫ eqToHom ⋯ = (s.proj a).φ i
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝³ : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst✝² : HasProduct X
inst✝¹ : HasProduct fun i ↦ X ↑i
inst✝ : HasProduct fun i ↦ X ↑i
⊢ HasBinaryProduct (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)

Tactic:
by
  classical exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

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

Goal state before:
pp: case refine_1
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j✝ j'✝ : J
g : j✝ ⟶ j'✝
y : (F.obj (op j'✝)).obj j✝
⊢ (hom ((G.map g.op).app j✝)) ((hom ((f.app (op j'✝)).app j✝)) y) =
    (hom ((f.app (op j✝)).app j✝)) ((Hom.hom ((F.map g.op).app j✝)) y)

Tactic:
simp only [← NatTrans.comp_app_apply, f.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor.map (ρ.map f)
⊢ W₂ (f ≫ i.app Y)

Tactic:
exact W₂.comp_mem _ _ hf (hi Y)

Goal state after:
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
⊢ W.HasLocalization

Tactic:
have : (inducedFunctor L.obj).EssSurj := ⟨fun Y ↦ ⟨_, ⟨L.objObjPreimageIso Y⟩⟩⟩

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
⊢ W.HasLocalization
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option.refine_1.some
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {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)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
f : (X₁, X₂) ⟶ (Y₁, Y₂)
hf₁ : W none f.1
hf₂ : MorphismProperty.pi (fun j ↦ W (some j)) f.2
i : J
⊢ W (some i) ((Pi.optionEquivalence C).inverse.map f (some i))

Tactic:
· apply hf₂

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro W X Y Z ⟨f⟩ ⟨g⟩ ⟨h⟩

Goal state after:
case mk.mk.mk
C : Type u
W X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : Quotient (W.setoidHom X)
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : Quotient (X.setoidHom Y)
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝ : Quotient (Y.setoidHom Z)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.comp ⋯ (Quotient.map₂ Hom.comp ⋯ (Quot.mk (⇑(W.setoidHom X)) f) (Quot.mk (⇑(X.setoidHom Y)) g))
      (Quot.mk (⇑(Y.setoidHom Z)) h) =
    Quotient.map₂ Hom.comp ⋯ (Quot.mk (⇑(W.setoidHom X)) f)
      (Quotient.map₂ Hom.comp ⋯ (Quot.mk (⇑(X.setoidHom Y)) g) (Quot.mk (⇑(Y.setoidHom Z)) h))
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  ((curriedTensorPre F).map (εIso L).inv ≫ (curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D)).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj (𝟙_ C)) ≫ (curriedTensorPost F).map (εIso L).inv).app (L.obj X₂)
⊢ (LaxMonoidal.ofBifunctor.leftMapₗ F).app (L.obj X₂) =
    (LaxMonoidal.ofBifunctor.topMapₗ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
          (curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapₗ F).app
      (L.obj X₂)

Tactic:
dsimp [e] at this ⊢

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  F.map (η L) ▷ F.obj (L.obj X₂) ≫ ((curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D)).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj (𝟙_ C))).app (L.obj X₂) ≫ F.map (η L ▷ L.obj X₂)
⊢ (λ_ (F.obj (L.obj X₂))).hom =
    (ε G ≫ (Lifting.iso L W G F).inv.app (𝟙_ C) ≫ F.map (η L)) ▷ F.obj (L.obj X₂) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D)).app (L.obj X₂) ≫ F.map (λ_ (L.obj X₂)).hom
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
this :
  ((curriedTensorPre F).obj (L.obj X₁)).map (εIso L).inv ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (𝟙_ D) =
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj (𝟙_ C)) ≫
      ((curriedTensorPost F).obj (L.obj X₁)).map (εIso L).inv
⊢ (LaxMonoidal.ofBifunctor.leftMapᵣ F).app (L.obj X₁) =
    (LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
          ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫
            LaxMonoidal.ofBifunctor.bottomMapᵣ F).app
      (L.obj X₁)

Tactic:
dsimp [e] at this ⊢

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ : C
this :
  F.obj (L.obj X₁) ◁ F.map (η L) ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (𝟙_ D) =
    ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj (𝟙_ C)) ≫ F.map (L.obj X₁ ◁ η L)
⊢ (ρ_ (F.obj (L.obj X₁))).hom =
    F.obj (L.obj X₁) ◁ (ε G ≫ (Lifting.iso L W G F).inv.app (𝟙_ C) ≫ F.map (η L)) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (𝟙_ D) ≫ F.map (ρ_ (L.obj X₁)).hom