mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Topology

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

Tactic:
intro ⟨U, hU, hUopen, hUone⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
⊢ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S
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)
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)

Tactic:
have (i : ι) : DiscreteTopology (f i).V := ⟨rfl⟩

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 ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
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
⊢ ∃ g, g • x = y

Tactic:
by
    let F' : C ⥤ FintypeCat.{u₂} := F ⋙ FintypeCat.uSwitch.{w, u₂}
    let : FiberFunctor F' := FiberFunctor.comp_right _
    let e (Y : C) : F'.obj Y ≃ F.obj Y := (F.obj Y).uSwitchEquiv
    set x' : F'.obj X := (e X).symm x with hx'
    set y' : F'.obj X := (e X).symm y with hy'
    obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'
    let gapp (Y : C) : F.obj Y ≅ F.obj Y := FintypeCat.equivEquivIso <|
      (e Y).symm.trans <| (FintypeCat.equivEquivIso.symm (g'.app Y)).trans (e Y)
    let g : F ≅ F := NatIso.ofComponents gapp <| fun {X Y} f ↦ by
      ext x
      dsimp [gapp, e]
      erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
      rw [← Functor.comp_map]
      erw [← NatTrans.naturality_apply, FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
      rfl
    refine ⟨g, show (gapp X).hom x = y from ?_⟩
    simp [gapp, ← hx', hg', hy', Equiv.apply_symm_apply]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
rintro h
    apply @sInf_le (Subgroupoid C) _
    exact ⟨h, Sn⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
⊢ HasWidePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
    (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).left) fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom

Tactic:
dsimp
  have : HasProduct fun (x : Fin (n + 1)) ↦ U := ⟨⟨_, U.isLimitPowerFan (Fin (n + 1))⟩⟩
  exact hasWidePullback_of_isTerminal _ (isTerminalIncl _ hT)

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

Goal state before:
pp: case pos
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
h : P b
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b

pp: case neg
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
h : ¬P b
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b

Tactic:
· simp [← h₁, dif_pos h]

Goal state after:
case neg
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
h : ¬P b
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
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
inst✝³ : Category.{v₄, u₄} A'
inst✝² : Category.{v₅, u₅} B'
inst✝¹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
⊢ inv f.right = (inv f).right

Tactic:
symm
  apply IsIso.eq_inv_of_inv_hom_id
  simp [← CatCospanTransform.category_comp_right]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
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'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ η ▷ φ ≫ inv η ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
by simp [← comp_whiskerRight]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
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'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ inv η ▷ φ ≫ η ▷ φ = 𝟙 (ψ'.comp φ)

Tactic:
by simp [← comp_whiskerRight]

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

Goal state before:
pp: case h_option.refine_1
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
⊢ (W none).prod (MorphismProperty.pi fun j ↦ W (some j)) ≤
    (MorphismProperty.pi W).isoClosure.inverseImage (Pi.optionEquivalence C).symm.functor

Tactic:
intro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ f ⟨hf₁, hf₂⟩

Goal state after:
case h_option.refine_1
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
⊢ (MorphismProperty.pi W).isoClosure.inverseImage (Pi.optionEquivalence C).symm.functor f
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: 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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ ((curriedTensorPost F).obj Y₁).map e₂.hom
h₂ :
  ∀ (X : D),
    ((curriedTensorPre F).map e₁.hom ≫ (curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁ ≫ (curriedTensorPost F).map e₁.hom).app X
⊢ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))

Tactic:
dsimp at h₁ h₂ ⊢

Goal state after:
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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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 D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)))

Tactic:
have w₂ : ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)) =
        ((yoneda.obj (R.obj c)).mapIso (β_ _ _)).hom ≫
          ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c)) ≫
            ((yoneda.obj (R.obj c)).mapIso (β_ _ _)).hom := by ext; simp

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 D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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 D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ tensorLeft c ⊣ R ⋙ ihom (R.obj c) ⋙ L

Tactic:
refine ((ihom.adjunction (R.obj c)).comp adj).restrictFullyFaithful
      (FullyFaithful.ofFullyFaithful R)
      (FullyFaithful.id _) ?_ ?_

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C

case refine_2
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (tensorRight L.X).map (P.actRight ▷ Q.X) ≫
      (α_ P.X Q.X L.X).hom ≫
        P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
            ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) =
    (tensorRight L.X).map ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (α_ P.X Q.X L.X).hom ≫
        P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
            ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)

Tactic:
dsimp; dsimp [TensorBimod.X]
        slice_lhs 1 2 => rw [associator_naturality_left]
        slice_lhs 2 3 => rw [← whisker_exchange]
        slice_lhs 3 4 => rw [coequalizer.condition]
        slice_lhs 2 3 => rw [associator_naturality_right]
        slice_lhs 3 4 =>
          rw [← whiskerLeft_comp, TensorBimod.whiskerLeft_π_actLeft, whiskerLeft_comp]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
V : Type u₂
inst✝² : Category.{v₂, u₂} V
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalCategory V
F G : C ⊛⥤ V
α β : F ⟶ G
h : α.natTrans = β.natTrans
⊢ α = β

Tactic:
by
  cases α
  cases β
  grind

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ 𝒮 ≫ Δ = Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)

Tactic:
by
  -- Again, it is a "left inverse equals right inverse" argument in the convolution monoid.
  apply left_inv_eq_right_inv
    (M := Conv A (A ⊗ A))
    (a := Δ[A])
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, tensor_whiskerLeft, MonObj.tensorObj.mul_def, Category.assoc,
      MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₁ A
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [whiskerLeft_comp, tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc,
      MonObj.tensorObj.mul_def, MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₂ A

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

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ R.X ◁ coequalizer.desc P.actLeft ⋯

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft

Tactic:
rw [← whiskerLeft_comp, coequalizer.π_desc]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ P.actLeft

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ R.X ◁ coequalizer.desc P.actRight ⋯

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft

Tactic:
rw [← whiskerLeft_comp, coequalizer.π_desc]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ P.actRight

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actLeft