mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η ε ⊗≫ rightZigzag η ε = rightZigzag η ε

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ leftZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (λ_ (𝟙 a)).hom ≫ (ρ_ (𝟙 a)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ rightZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom ≫ (λ_ (𝟙 a)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
⊢ μ ≫
      Hom.asOver
        (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
        (Spec (of S)) =
    (Hom.asOver (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
          (Spec (of S)) ⊗ₘ
        Hom.asOver
          (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
          (Spec (of S))) ≫
      μ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
G : Over (Spec R)
⊢ (algSpec R).essImage G ↔ IsAffine G.left

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
G : Mon (Over (Spec R))
⊢ (bialgSpec R).essImage G ↔ IsAffine G.X.left

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
G : Grp (Over (Spec R))
⊢ (hopfSpec R).essImage G ↔ IsAffine G.X.left

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : Adj B
α β : a ⟶ b
p : Hom₂ α β
⊢ (conjugateEquiv β.adj α.adj).symm p.τr = p.τl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ d : Adj B
a b c : a✝ ⟶ b✝
x : Hom₂ a b
y : Hom₂ b c
⊢ (conjugateEquiv c.adj a.adj) (x.τl ≫ y.τl) = y.τr ≫ x.τr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : Adj B
α β : a ⟶ b
x y : α ⟶ β
hl : x.τl = y.τl
⊢ x.τr = y.τr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj) el.hom = er.hom
⊢ (conjugateEquiv α.adj β.adj) el.inv = er.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (𝟙 a ≫ α).adj) (λ_ α.l).hom = (ρ_ α.r).symm.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (α ≫ 𝟙 b).adj) (ρ_ α.l).hom = (λ_ α.r).symm.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
β β' : b ⟶ c
y : β ⟶ β'
⊢ (conjugateEquiv (α ≫ β').adj (α ≫ β).adj) (α.l ◁ y.τl) = y.τr ▷ α.r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α α' : a ⟶ b
x : α ⟶ α'
β : b ⟶ c
⊢ (conjugateEquiv (α' ≫ β).adj (α ≫ β).adj) (x.τl ▷ β.l) = β.r ◁ x.τr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
by
      simp_rw [left_triangle]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑C
⊢ F.toFunctor.map (adj.unit.toNatTrans.app X) ≫ adj.counit.toNatTrans.app (F.toFunctor.obj X) = 𝟙 (F.toFunctor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑D
⊢ adj.unit.toNatTrans.app (G.toFunctor.obj X) ≫ G.toFunctor.map (adj.counit.toNatTrans.app X) = 𝟙 (G.toFunctor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v, u} D
inst✝ : Category.{v, u} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
⊢ adj.toCat.comp adj'.toCat = (adj.comp adj').toCat

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
⊢ Adjunction.ofCat (adj.comp adj') = (Adjunction.ofCat adj).comp (Adjunction.ofCat adj')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
⊢ ((mateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
⊢ ((conjugateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
W : Opens ↥U
x✝¹ : X
x✝ : x✝¹ ∈ { carrier := Subtype.val '' ↑W, is_open' := ⋯ }
⊢ x✝¹ ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
⊢ ((𝟭 (Over U)).obj V).left =
    (({ obj := fun V ↦ { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ }, map := fun {X_1 Y} f ↦ homOfLE ⋯,
              map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun W ↦ Over.mk (homOfLE ⋯), map := fun {X_1 Y} f ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯,
              map_comp := ⋯ }).obj
        V).left

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Opens ↥U
⊢ ({ obj := fun W ↦ Over.mk (homOfLE ⋯), map := fun {X_1 Y} f ↦ Over.homMk (homOfLE ⋯) ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
          { obj := fun V ↦ { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ }, map := fun {X_1 Y} f ↦ homOfLE ⋯,
            map_id := ⋯, map_comp := ⋯ }).obj
      V =
    (𝟭 (Opens ↥U)).obj V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
⊢ Sieve.functorPushforward U.overEquivalence.functor S ∈
      (Opens.grothendieckTopology ↥U) (U.overEquivalence.functor.obj V) ↔
    S ∈ ((Opens.grothendieckTopology X).over U) V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Module

Goal state before:
pp: X : TopCat
U : Opens ↑X
R : TopCat.Sheaf RingCat X
⊢ SheafOfModules (Sheaf.over R U) ≌ SheafOfModules (U.sheafRestrict.obj R)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
whisker_exchange

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ (adj₁.counit ▷ 𝟙 b ≫ 𝟙 b ◁ adj₂.unit) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ (fun β ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β)
      ((fun γ ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom) γ) =
    𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ 𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) = γ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
simp_rw [right_triangle]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun γ ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun β ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b c : B
f : a ⟶ b
g : b ⟶ a
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ (adj.counit ▷ (r ≫ g) ≫ 𝟙 c ◁ β) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b c : B
f : a ⟶ b
g : b ⟶ a
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β = β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun γ ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun β ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ (fun γ ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom)
      ((fun α ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r) α) =
    𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom

Tactic:
← whisker_exchange η.hom (f ◁ ε.inv)

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α = α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ (fun α ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r)
      ((fun γ ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom) γ) =
    𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r)

Tactic:
by

Goal state after: