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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ ((fun f ↦ { f := X.a ≫ G.map f, h := ⋯ }) ((fun g ↦ g.f ≫ G.ε.app Y) g)).f = g.f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f
Module: Mathlib.CategoryTheory.Monad.Products

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasBinaryCoproducts C
X✝ Y✝ : (coprodMonad X).Algebra
f : X✝ ⟶ Y✝
⊢ (Under.mk (coprod.inl ≫ X✝.a)).hom ≫ f.f = (Under.mk (coprod.inl ≫ Y✝.a)).hom

Tactic:
by simp [← dsimp% f.h]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')

Tactic:
dsimp

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ ((↑b * ↑b') • g a') = g (b • a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
s : ↥S
p : LocalizedModule S M
⊢ ∀ (m : M) (s_1 : ↥S),
    ↑{ val := (algebraMap R (End R (LocalizedModule S M))) ↑s, inv := LocalizedModule.divBy s, val_inv := ⋯,
            inv_val := ⋯ }
        (LocalizedModule.mk m s_1) =
      ((algebraMap R (End R (LocalizedModule S M))) ↑s) (LocalizedModule.mk m s_1)

Tactic:
by
          intros
          rfl

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ ↑⋯.unit⁻¹ (f (a, b).1) = ↑⋯.unit⁻¹ (f (a', b').1)

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom =
    (tensorProdObjIsoPushoutObj S A).hom ≫ (Under.pushout (ofHom (algebraMap ↑R ↑S))).map f

Tactic:
dsimp

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom =
    (tensorProdObjIsoPushoutObj S A).hom ≫
      Under.homMk
        (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
          (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
        ⋯
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ Hom.left
      ((fun u ↦ homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯)
        ((fun v ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v)) =
    Hom.left v

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ = Hom.left v
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ Hom.right
      ((fun v ↦ homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯)
        ((fun u ↦ homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯) u)) =
    Hom.right u

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = Hom.right u
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
⊢ (fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f ↦ (initial.to (StructuredArrow.mk f)).right) f) = f

Tactic:
let B' : StructuredArrow A G := StructuredArrow.mk f
    apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)

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

Goal state before:
pp: case h₁
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).left =
    (s.π.app j).left

Tactic:
exact h₁.fac ((fst _ _).mapCone s) j

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ IsIso f

Tactic:
refine ⟨ofHom ⟨1, rfl, by simp⟩, ?_, ?_⟩

Goal state after:
case refine_1
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})

case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M'
inst✝¹⁵ : AddCommMonoid M''
A : Type u_5
inst✝¹⁴ : CommSemiring A
inst✝¹³ : Algebra R A
inst✝¹² : Module A M'
inst✝¹¹ : IsLocalization S A
inst✝¹⁰ : Module R M
inst✝⁹ : Module R M'
inst✝⁸ : Module R M''
inst✝⁷ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
y : M₂
⊢ ∃ x, x.2 • y = (liftOfLE S₁ S₂ h f₁ f₂) x.1

Tactic:
obtain ⟨⟨y', s⟩, e⟩ := IsLocalizedModule.surj S₂ f₂ y
    exact ⟨⟨f₁ y', s⟩, by simpa⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)

Tactic:
rw [← F.map₂_comp, Iso.inv_hom_id, F.map₂_id]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) ≫
      (G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫
      (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.map₂ (η ▷ g)) ≫ G.map₂ (F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    (F.comp G.toPrelaxFunctor).map₂ (η ◁ η_1) ≫
        (G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g') =
      ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫
        (F.comp G.toPrelaxFunctor).map η ◁ (F.comp G.toPrelaxFunctor).map₂ η_1

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    G.map₂ (F.map₂ (η ◁ η_1)) ≫ G.map₂ (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g') =
      (G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (α_ f g h).hom ≫
      ((G.mapFunctor (F.obj a✝) (F.obj d✝)).map (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))) ≫
        (F.comp G.toPrelaxFunctor).map f ◁
          ((G.mapFunctor (F.obj b✝) (F.obj d✝)).map (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) =
    ((G.mapFunctor (F.obj a✝) (F.obj d✝)).map (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h)) ≫
      ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷
          (F.comp G.toPrelaxFunctor).map h ≫
        (α_ ((F.comp G.toPrelaxFunctor).map f) ((F.comp G.toPrelaxFunctor).map g)
            ((F.comp G.toPrelaxFunctor).map h)).hom

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ G.map₂ (F.map₂ (α_ f g h).hom) ≫
      (G.map₂ (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))) ≫
        G.map (F.map f) ◁ (G.map₂ (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) =
    (G.map₂ (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h)) ≫
      (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
        (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp (𝟙 a✝) f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f)) ≫
      ((G.mapFunctor (F.obj a✝) (F.obj a✝)).map (F.mapId a✝) ≫ G.mapId (F.obj a✝)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        (λ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ G.map₂ (F.map₂ (λ_ f).hom) =
    (G.map₂ (F.mapComp (𝟙 a✝) f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f)) ≫
      (G.map₂ (F.mapId a✝) ≫ G.mapId (F.obj a✝)) ▷ G.map (F.map f) ≫ (λ_ (G.map (F.map f))).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp f (𝟙 b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝))) ≫
      (F.comp G.toPrelaxFunctor).map f ◁ ((G.mapFunctor (F.obj b✝) (F.obj b✝)).map (F.mapId b✝) ≫ G.mapId (F.obj b✝)) ≫
        (ρ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ G.map₂ (F.map₂ (ρ_ f).hom) =
    (G.map₂ (F.mapComp f (𝟙 b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝))) ≫
      G.map (F.map f) ◁ (G.map₂ (F.mapId b✝) ≫ G.mapId (F.obj b✝)) ≫ (ρ_ (G.map (F.map f))).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g)) ≫ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) =
    (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g ≫
      G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ (G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹)) ≫ (F.comp G.toPrelaxFunctor).map₂ (f ◁ η) =
    (F.comp G.toPrelaxFunctor).map f ◁ (F.comp G.toPrelaxFunctor).map₂ η ≫
      G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ (G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ (F.comp G.toPrelaxFunctor).map h ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫
        (F.comp G.toPrelaxFunctor).map₂ (α_ f g h).hom =
    (α_ ((F.comp G.toPrelaxFunctor).map f) ((F.comp G.toPrelaxFunctor).map g) ((F.comp G.toPrelaxFunctor).map h)).hom ≫
      (F.comp G.toPrelaxFunctor).map f ◁ (G.mapComp (F.map g) (F.map h) ≫ G.map₂ (F.mapComp g h)) ≫
        G.mapComp (F.map f) (F.map (g ≫ h)) ≫ G.map₂ (F.mapComp f (g ≫ h))

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
    (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
      G.map (F.map f) ◁ (G.mapComp (F.map g) (F.map h) ≫ G.map₂ (F.mapComp g h)) ≫
        G.mapComp (F.map f) (F.map (g ≫ h)) ≫ G.map₂ (F.mapComp f (g ≫ h))
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).inv =
    (λ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (G.mapId (F.obj a✝) ≫ G.map₂ (F.mapId a✝)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        G.mapComp (F.map (𝟙 a✝)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a✝) f)

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ G.map₂ (F.map₂ (λ_ f).inv) =
    (λ_ (G.map (F.map f))).inv ≫
      (G.mapId (F.obj a✝) ≫ G.map₂ (F.mapId a✝)) ▷ G.map (F.map f) ≫
        G.mapComp (F.map (𝟙 a✝)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a✝) f)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).inv =
    (ρ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (F.comp G.toPrelaxFunctor).map f ◁ (G.mapId (F.obj b✝) ≫ G.map₂ (F.mapId b✝)) ≫
        G.mapComp (F.map f) (F.map (𝟙 b✝)) ≫ G.map₂ (F.mapComp f (𝟙 b✝))

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ G.map₂ (F.map₂ (ρ_ f).inv) =
    (ρ_ (G.map (F.map f))).inv ≫
      G.map (F.map f) ◁ (G.mapId (F.obj b✝) ≫ G.map₂ (F.mapId b✝)) ≫
        G.mapComp (F.map f) (F.map (𝟙 b✝)) ≫ G.map₂ (F.mapComp f (𝟙 b✝))
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (asIso (F.mapComp f g)).hom ≫ F.map f ◁ F.map₂ η ≫ (asIso (F.mapComp f h)).inv

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = (asIso (F.mapComp f✝ h)).hom ≫ F.map₂ η ▷ F.map h ≫ (asIso (F.mapComp g✝ h)).inv

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g✝ h)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    (asIso (F.mapComp (f ≫ g) h)).hom ≫
      (asIso (F.mapComp f g)).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫
          F.map f ◁ (asIso (F.mapComp g h)).inv ≫ (asIso (F.mapComp f (g ≫ h))).inv

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (g ≫ h))
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case sup
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I

Tactic:
obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx

Goal state after:
case sup
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case fst
X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
x : x✝¹.pt
⊢ ((ConcreteCategory.hom x✝).toFun x).1 =
    ((ConcreteCategory.hom
            (↾fun x ↦
              ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x))).toFun
        x).1

pp: case snd
X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
x : x✝¹.pt
⊢ ((ConcreteCategory.hom x✝).toFun x).2 =
    ((ConcreteCategory.hom
            (↾fun x ↦
              ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x))).toFun
        x).2

Tactic:
exacts [ConcreteCategory.congr_hom (w ⟨left⟩) x, ConcreteCategory.congr_hom (w ⟨right⟩) x]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ yoneda.map (Iso.refl (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).left).hom ≫
      ((𝟭 (CostructuredArrow yoneda F)).obj X).hom =
    (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).hom

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ yoneda.map (𝟙 X.left) ≫ X.hom = yonedaEquiv.symm (yonedaEquiv X.hom)