mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.kernel.isoModSerre = ObjectProperty.isLocal fun x ↦ x ∈ Set.range F.obj

Tactic:
ObjectProperty.isLocal_eq_inverseImage_isomorphisms 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✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.kernel.isoModSerre = (isomorphisms C).inverseImage G
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom ∘ₗ ConcreteCategory.hom q) a'' = a

Tactic:
← ModuleCat.hom_comp,

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom (q ≫ y.hom)) a'' = a
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom ∘ₗ ConcreteCategory.hom p) a'' = a

Tactic:
← ModuleCat.hom_comp,

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom (p ≫ x.hom)) a'' = a
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
ha : a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ a ∈ (ModuleCat.Hom.hom x.hom).range

Tactic:
obtain ⟨a', ha'⟩ := ha
    obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'
    refine ⟨p a'', ?_⟩
    dsimp at ha' ⊢
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, H, ModuleCat.hom_comp, LinearMap.comp_apply,
      ha'', ha']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P.epiModSerre (s ≫ Abelian.factorThruImage f)
⊢ s ≫ Abelian.factorThruImage f = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre (Abelian.factorThruCoimage f ≫ s)
⊢ Abelian.factorThruCoimage f ≫ s = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
exact ⟨Y', s, hs.1, eq⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝⁴ : Abelian C
inst✝³ : P.ContainsZero
inst✝² : P.IsClosedUnderKernels
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : Mono f
this : P.ι.PreservesMonomorphisms
⊢ f ≫ homMk (cokernel.π f.hom) = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝⁴ : Abelian C
inst✝³ : P.ContainsZero
inst✝² : P.IsClosedUnderKernels
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : Epi f
this : P.ι.PreservesEpimorphisms
⊢ homMk (kernel.ι f.hom) ≫ f = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f

Tactic:
cat_disch

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
x✝ : G
⊢ F.map (X✝.ρ x✝ ≫ h.preimage f.hom) = F.map (h.preimage f.hom ≫ Y✝.ρ x✝)

Tactic:
simp only [map_comp, map_preimage]

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
x✝ : G
⊢ F.map (X✝.ρ x✝) ≫ f.hom = f.hom ≫ F.map (Y✝.ρ x✝)
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s : BinaryCofan a b
⊢ pushout.desc (underlying.map (s.ι.app { as := WalkingPair.left }))
        (underlying.map (s.ι.app { as := WalkingPair.right })) ⋯ ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow =
    pushout.desc a.arrow b.arrow ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y)
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
        U.map (R.map g)) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y))
          ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩)) ≫
      R.map g

Tactic:
cat_disch

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

Goal state before:
pp: case vcomp_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η✝ : Hom₂ f✝ g✝
θ₁✝ θ₂✝ : Hom₂ g✝ h✝
a✝ : Rel θ₁✝ θ₂✝
a_ih✝ : liftHom₂ F θ₁✝ = liftHom₂ F θ₂✝
⊢ liftHom₂ F η✝ ≫ liftHom₂ F θ₁✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ₂✝

Tactic:
cat_disch

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

Goal state before:
pp: case vcomp_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η₁✝ η₂✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
a✝ : Rel η₁✝ η₂✝
a_ih✝ : liftHom₂ F η₁✝ = liftHom₂ F η₂✝
⊢ liftHom₂ F η₁✝ ≫ liftHom₂ F θ✝ = liftHom₂ F η₂✝ ≫ liftHom₂ F θ✝

Tactic:
cat_disch

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

Goal state before:
pp: case id_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (liftHom F f✝) ≫ liftHom₂ F η✝ = liftHom₂ F η✝

Tactic:
cat_disch

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

Goal state before:
pp: case comp_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ≫ 𝟙 (liftHom F g✝) = liftHom₂ F η✝

Tactic:
cat_disch

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y),
    (𝟭 (a ⟶ b)).map f ≫ ((λ_ Y).symm ≪≫ normalizeIso nil Y).hom =
      ((λ_ X).symm ≪≫ normalizeIso nil X).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f

Tactic:
by
      intro f g η
      erw [leftUnitor_inv_naturality_assoc, assoc]
      congr 1
      exact normalize_naturality nil η

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

Goal state before:
pp: case assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ h✝ i✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
ι✝ : Hom₂ h✝ i✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ≫ liftHom₂ F ι✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ✝ ≫ liftHom₂ F ι✝

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ : Hom a✝¹ b✝
g✝ h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ g✝ h✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom F f✝ ◁ liftHom₂ F η✝ = liftHom F f✝ ◁ liftHom₂ F η'✝

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_left_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom F f✝ ◁ 𝟙 (liftHom F g✝) = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_left_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ h✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) = liftHom F f✝ ◁ liftHom₂ F η✝ ≫ liftHom F f✝ ◁ liftHom₂ F θ✝

Tactic:
cat_disch

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

Goal state before:
pp: case id_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (F.obj a✝) ◁ liftHom₂ F η✝ = (λ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (λ_ (liftHom F g✝)).inv

Tactic:
cat_disch

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

Goal state before:
pp: case comp_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ h'✝ : Hom c✝ d✝
η✝ : Hom₂ h✝ h'✝
⊢ (liftHom F f✝ ≫ liftHom F g✝) ◁ liftHom₂ F η✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom F g✝ ◁ liftHom₂ F η✝ ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h'✝)).inv

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ g✝ : Hom a✝¹ b✝
h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ f✝ g✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F η✝ ▷ liftHom F h✝ = liftHom₂ F η'✝ ▷ liftHom F h✝

Tactic:
cat_disch

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

Goal state before:
pp: case id_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ 𝟙 (liftHom F f✝) ▷ liftHom F g✝ = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)

Tactic:
cat_disch

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

Goal state before:
pp: case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ▷ liftHom F i✝ = liftHom₂ F η✝ ▷ liftHom F i✝ ≫ liftHom₂ F θ✝ ▷ liftHom F i✝

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ▷ 𝟙 (F.obj b✝) = (ρ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (ρ_ (liftHom F g✝)).inv

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F η✝ ▷ (liftHom F g✝ ≫ liftHom F h✝) =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫
      liftHom₂ F η✝ ▷ liftHom F g✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f'✝) (liftHom F g✝) (liftHom F h✝)).hom

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ (liftHom F f✝ ◁ liftHom₂ F η✝) ▷ liftHom F h✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom₂ F η✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f✝) (liftHom F g'✝) (liftHom F h✝)).inv

Tactic:
cat_disch

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

Goal state before:
pp: case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ liftHom₂ F θ✝ ≫ liftHom₂ F η✝ ▷ liftHom F i✝ =
    liftHom₂ F η✝ ▷ liftHom F h✝ ≫ liftHom F g✝ ◁ liftHom₂ F θ✝

Tactic:
cat_disch

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

Goal state before:
pp: case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv =
    𝟙 ((liftHom F f✝ ≫ liftHom F g✝) ≫ liftHom F h✝)

Tactic:
cat_disch

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

Goal state before:
pp: case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom =
    𝟙 (liftHom F f✝ ≫ liftHom F g✝ ≫ liftHom F h✝)

Tactic:
cat_disch

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

Goal state before:
pp: case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).hom ≫ (λ_ (liftHom F f✝)).inv = 𝟙 (𝟙 (F.obj a✝) ≫ liftHom F f✝)

Tactic:
cat_disch

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

Goal state before:
pp: case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).inv ≫ (λ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)

Tactic:
cat_disch

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

Goal state before:
pp: case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).hom ≫ (ρ_ (liftHom F f✝)).inv = 𝟙 (liftHom F f✝ ≫ 𝟙 (F.obj b✝))

Tactic:
cat_disch

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

Goal state before:
pp: case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).inv ≫ (ρ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)

Tactic:
cat_disch

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

Goal state before:
pp: case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ▷ liftHom F i✝ ≫
      (α_ (liftHom F f✝) (liftHom F g✝ ≫ liftHom F h✝) (liftHom F i✝)).hom ≫
        liftHom F f✝ ◁ (α_ (liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom =
    (α_ (liftHom F f✝ ≫ liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom ≫
      (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝ ≫ liftHom F i✝)).hom

Tactic:
cat_disch

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

Goal state before:
pp: case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ (α_ (liftHom F f✝) (𝟙 (F.obj b✝)) (liftHom F g✝)).hom ≫ liftHom F f✝ ◁ (λ_ (liftHom F g✝)).hom =
    (ρ_ (liftHom F f✝)).hom ▷ liftHom F g✝

Tactic:
cat_disch

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

Goal state before:
pp: case f
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
a✝ : Hom₂ g h
⊢ Quot.lift (liftHom₂ F) ⋯ (f ◁ Quot.mk Rel a✝) =
    (Iso.refl (liftHom F (f ≫ g))).hom ≫
      liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
cat_disch

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

Goal state before:
pp: case f
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝¹ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝¹ ⟶ b✝
h : b✝ ⟶ c✝
a✝ : Hom₂ f✝ g✝
⊢ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝ ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
      Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ▷ liftHom F h ≫ 𝟙 (liftHom F g✝ ≫ liftHom F h)

Tactic:
cat_disch

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

Goal state before:
pp: case h
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝¹ b✝¹ c✝ : FreeBicategory B
f✝ g✝ : a✝¹ ⟶ b✝¹
η : f✝ ⟶ g✝
h : b✝¹ ⟶ c✝
a✝ b✝ : Hom₂ f✝ g✝
p✝ : Rel a✝ b✝
⊢ ⋯ = ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ η.naturality (𝟙 a) ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]; simp

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

Goal state before:
pp: case mk.mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
base✝¹ : a.base ⟶ b.base
fiber✝¹ : (F.map base✝¹.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
base✝ : a.base ⟶ b.base
fiber✝ : (F.map base✝.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
hfg₁ : base✝¹ = base✝
hfg₂ : eqToHom ⋯ ≫ fiber✝¹ = fiber✝
⊢ { base := base✝¹, fiber := fiber✝¹ } = { base := base✝, fiber := fiber✝ }

Tactic:
cat_disch

Goal state after: