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

Goal state before:
pp: case h.inr
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₂
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inr val✝))

Tactic:
· exact hf₂ _

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
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
⊢ (((incl F).op ⋙ coyoneda).map (Opposite.op { val := f, comp := hf }) ≫
      match Opposite.op { obj := B, pt := b, isGalois := isGalois✝ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) =
    (match Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) ≫
      ((const (PointedGaloisObject F)ᵒᵖ).obj (F ⋙ FintypeCat.incl)).map (Opposite.op { val := f, comp := hf })

Tactic:
ext Y (g : (A : C) ⟶ Y)
      suffices h : F.map g (F.map f b) = F.map g a by simpa
      rw [hf]

Goal state after:
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
⊢ (F.obj X).obj ≃ (F.obj X).obj

Tactic:
apply Equiv.ofBijective σ

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 := ⋯
⊢ Function.Bijective σ
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

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

Tactic:
· intro ⟨U, hU, hUopen, hUone⟩
      obtain ⟨I, _, hc, hmem⟩ := exists_set_ker_evaluation_subset_of_isOpen F hUone hUopen
      let P : C := ∏ᶜ fun X : I ↦ X.val
      obtain ⟨A, a, hgal, hbij⟩ := exists_galois_representative F P
      refine ⟨⟨A, a, hgal⟩, trivial, ?_⟩
      intro t (ht : t.hom.app A a = a)
      apply hU
      apply hmem
      have (X : I) : IsConnected X.val := hc X.val X.property
      have (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
      intro X
      ext x
      simp only [FintypeCat.id_apply]
      obtain ⟨z, rfl⟩ :=
        surjective_of_nonempty_fiber_of_isConnected F (Pi.π (fun X : I ↦ X.val) X) x
      obtain ⟨f, rfl⟩ := hbij.surjective z
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply, ht]

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

Goal state before:
pp: case hst
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
⊢ (⋂ i ∈ s, cl i).Nonempty

Tactic:
use gs

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 := ⋯
c : Set G := ⋯
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
⊢ gs ∈ ⋂ i ∈ s, cl i
Module: Mathlib.CategoryTheory.Galois.EssSurj

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

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)
a✝ : Aut F
⊢ (ConcreteCategory.hom (u.inv ≫ (coconeQuotientDiag h u hUinV).ι.app j ≫ coconeQuotientDiagDesc h u hUinV s).hom)
      ⟦a✝⟧ =
    (ConcreteCategory.hom (u.inv ≫ s.ι.app j).hom) ⟦a✝⟧
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
· apply S.inv

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d

Tactic:
exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d)

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ d ∈ (im φ hφ).objs ↔ ∃ c, φ.obj c = d

Tactic:
simp only [im, mem_map_objs_iff, mem_top_objs, true_and]

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
⊢ Function.Surjective φ.obj

Tactic:
by
  rintro d
  rw [← mem_im_objs_iff _ hφ, hφ']
  apply mem_top_objs

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft eᵣ.hom =
    (Prod.fst C D).whiskerLeft eₗ.hom ≫ whiskerRight (edgeTransform C D) G

Tactic:
by simpa using h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : (hom (Limits.prod.fst.app a)) z = (hom (Limits.prod.fst.app a)) w
h2 : (hom (Limits.prod.snd.app a)) z = (hom (Limits.prod.snd.app a)) w
⊢ z = w

Tactic:
apply Equiv.injective (binaryProductEquiv F G a)
  aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂

Tactic:
simpa using h₁ =≫ h₁₂.p₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y

Tactic:
exact ⟨_, _, r_ne_s⟩

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

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
⊢ (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)

Tactic:
let E := Pi.equivalenceOfEquiv C₂ e

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ 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₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
⊢ (Functor.pi L₂).IsLocalization (MorphismProperty.pi W₂)
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ T.η.app X.of ≫ T.map f.of ≫ T.μ.app Y.of = f.of

Tactic:
rw [← T.η.naturality_assoc f.of, T.left_unit]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ (𝟭 C).map f.of ≫ 𝟙 ((𝟭 C).obj (T.obj Y.of)) = f.of
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ (𝟭 (KleisliCat m)).map f ≫ (Iso.refl Y✝).hom =
    (Iso.refl X✝).hom ≫
      ({ obj := fun X ↦ { of := X }, map := fun {X Y} f ↦ { of := ↾f }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun X ↦ X.of, map := fun {X Y} f x ↦ (ConcreteCategory.hom f.of) x, map_id := ⋯,
              map_comp := ⋯ }).map
        f

Tactic:
change f >=> pure = pure >=> f

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ f >=> pure = pure >=> f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 ((𝟭 C).obj A.A))

Tactic:
exact congr_arg F.map A.unit

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
d d' : D
f : d ⟶ d'
⊢ (λₗ d).inv ≫ 𝟙_ C ⊴ₗ f = f ≫ (λₗ d').inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

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✝ : MonoidalRightAction C D
d d' : D
f : d ⟶ d'
⊢ (ρᵣ d).inv ≫ f ⊵ᵣ 𝟙_ C = f ≫ (ρᵣ d').inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

Goal state after:
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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      adj.unit.app ((ihom d).obj (R.obj c)) ▷ d ≫
        (L ⋙ R).obj ((ihom d).obj (R.obj c)) ◁ adj.unit.app d ≫
          adj.unit.app ((L ⋙ R).obj ((ihom d).obj (R.obj c)) ⊗ (L ⋙ R).obj d) ≫
            inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))) ≫
              R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom) ≫
                R.map (L.map ((ihom.ev d).app (R.obj c))) ≫ inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
slice_lhs 2 3 =>
    simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]

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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((((adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d) ≫
                adj.unit.app ((L ⋙ R).obj ((ihom d).obj (R.obj c)) ⊗ (L ⋙ R).obj d)) ≫
              inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).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
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'))
⊢ [∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c))),
      ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c)),
      ∀ (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

Tactic:
tfae_have 4 → 1
  | _, _, _ => by
    -- It is enough to show that the unit is a split monomorphism, and the retraction is given
    -- by `adjRetraction` above.
    let _ : Reflective R := { L := L, adj := adj }
    have : IsIso adj.toMonad.μ := μ_iso_of_reflective (R := R)
    dsimp
    rw [← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit]
    exact ⟨⟨adjRetraction adj _ _, adjRetraction_is_retraction adj _ _⟩⟩

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)))
⊢ [∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c))),
      ∀ (c : C) (d : D), IsIso ((pre (adj.unit.app d)).app (R.obj c)),
      ∀ (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
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst✝¹ : F.Full
inst✝ : F.Faithful
B : D
⊢ IsIso ((frobeniusMorphism F h A).natTrans.app B)

Tactic:
dsimp [frobeniusMorphism]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst✝¹ : F.Full
inst✝ : F.Faithful
B : D
⊢ IsIso ((prodComparisonNatTrans L (F.obj A)).app B ≫ h.counit.app A ▷ L.obj B)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      (reflector i).obj A ◁ ((reflector i).map (η.app (A ⟹ i.obj B)) ≫ ε.app (L.obj (A ⟹ i.obj B))) ≫
        inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))

Tactic:
ir.left_triangle_components,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      (reflector i).obj A ◁ 𝟙 ((reflector i).obj (A ⟹ i.obj B)) ≫
        inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Tactic:
← BraidedCategory.braiding_naturality_left_assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((reflectorAdjunction i).unit.app A ▷ B ≫
        (β_ (i.obj ((reflector i).obj A)) B).hom ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B