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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a✝¹ a : B
t : a ⟶ a
inst✝ : Comonad t
a✝ b✝ c✝ d✝ : LocallyDiscrete (Discrete Unit)
x✝² : a✝ ⟶ b✝
x✝¹ : b✝ ⟶ c✝
x✝ : c✝ ⟶ d✝
⊢ 𝟙 t ≫ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a : B
t : a ⟶ a
inst✝ : Comonad t
⊢ Δ = Δ

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a✝ b✝ c✝ : Pith B
f✝ g✝ : a✝ ⟶ b✝
h✝ i✝ : b✝ ⟶ c✝
η : f✝ ⟶ g✝
θ : h✝ ⟶ i✝
⊢ { iso := f✝.of ◁ᵢ θ.iso } ≫ { iso := η.iso ▷ᵢ i✝.of } = { iso := η.iso ▷ᵢ h✝.of } ≫ { iso := g✝.of ◁ᵢ θ.iso }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
⊢ IsLocallyGroupoid (Pith B)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Opposites

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ d✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g g' : b✝ ⟶ c✝
η : g ⟶ g'
i : c✝ ⟶ d✝
⊢ i.unop ◁ (op2 (η.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop g.unop f.unop).op2_unop.symm.hom.unop2 ≫
      (op2 ((op2 (i.unop ◁ η.unop2)).unop2 ▷ f.unop) ≫ (α_ i.unop g'.unop f.unop).op2_unop.symm.inv).unop2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Opposites

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ d✝ e✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
⊢ (op2 (i.unop ◁ (α_ h.unop g.unop f.unop).op2_unop.symm.hom.unop2)).unop2 ≫
      ((α_ i.unop (g ≫ h).unop f.unop).op2_unop.symm.hom ≫
          op2 ((α_ i.unop h.unop g.unop).op2_unop.symm.hom.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop h.unop (f ≫ g).unop).op2_unop.symm.hom.unop2 ≫ (α_ (h ≫ i).unop g.unop f.unop).op2_unop.symm.hom.unop2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Opposites

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (α_ g.unop (𝟙 b✝).unop f.unop).op2_unop.symm.hom.unop2 ≫ (op2 ((ρ_ g.unop).op2_unop.hom.unop2 ▷ f.unop)).unop2 =
    g.unop ◁ (λ_ f.unop).op2_unop.hom.unop2

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
⊢ ∀ (s : LeftExtension f (𝟙 a ≫ h)) (τ : (LeftExtension.mk u adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
⊢ leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
Wₗ Wᵣ : MorphismProperty C
c c' : C
S S' : Span Wₗ Wᵣ c c'
f g : S ⟶ S'
h : f.hom = g.hom
⊢ f = g

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag t.unit ε = (ρ_ t.extension).hom ≫ (λ_ t.extension).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ ((LeftLift.mk f adj.unit).whisker h).unit ≫ (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ▷ u =
    𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
⊢ h ◁ adj.unit ⊗≫ τ ▷ u = s.unit

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (τ ▷ (u ≫ f) ≫ s.lift ◁ adj.counit) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right (homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
⊢ ∀ (s : LeftLift u (h ≫ 𝟙 a)) (τ : (LeftLift.mk f adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
⊢ rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' f (𝟙 b₁) f ⋯ = (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).inv = F.map f ◁ (F.mapId b₁).hom ≫ (ρ_ (F.map f)).hom

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (t.lift ≫ u) ◁ t.unit) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' (𝟙 b₀) f f ⋯ = (λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).inv = (F.mapId b₀).hom ▷ F.map f ≫ (λ_ (F.map f)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f hf).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ f₀₁ ≫ f₁₃ = f

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ leftZigzag t.unit ε = (λ_ t.lift).hom ≫ (ρ_ t.lift).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
⊢ t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
    (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (g ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
by

Goal state after: