mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op ≫ (pullbackIsoOpPushout f₁.op f₂.op).inv =
    (pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯

Tactic:
ext <;> simp [← op_comp]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max u w} (Quot F)
⊢ IsColimit (colimitCocone F)

Tactic:
refine isColimit_of_bijective_desc F _ ?_

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max u w} (Quot F)
⊢ Function.Bijective ⇑(Quot.desc F (colimitCocone F))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• x.fst ^ i.succ)) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n✝ + 1))).sum

Tactic:
pow_succ

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• (x.fst ^ i * x.fst))) (List.range (n✝ + 1))).sum =
    (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n✝ + 1))).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ 0⁻¹ = fst 0

Tactic:
fst_zero,

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ 0⁻¹ = 0
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.rTensor B counit ∘ₗ comul = (TensorProduct.mk R R B) 1

Tactic:
by
    simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
    ext x
    simp [← (ℛ R _).eq]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.lTensor B counit ∘ₗ comul = (TensorProduct.mk R B R).flip 1

Tactic:
by
    simp_rw [(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,
      ← (f.toLinearEquiv.comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul, ← LinearMap.comp_assoc,
      f.toLinearEquiv.comp_toLinearMap_symm_eq]
    ext x
    simp [← (ℛ R _).eq]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom g) x✝ + (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ =
    (Hom.hom g) x✝ + (Hom.hom g) y✝

Tactic:
ih2

Goal state after:
case add
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
ih1 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) x✝ = (Hom.hom g) x✝
ih2 : (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) y✝ = (Hom.hom g) y✝
⊢ (Hom.hom g) x✝ + (Hom.hom g) y✝ = (Hom.hom g) x✝ + (Hom.hom g) y✝
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ toBoolAlg (f (ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b)) =
    toBoolAlg (f (ofBoolAlg a)) ⊔ toBoolAlg (f (ofBoolAlg b))

Tactic:
simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
by
  rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]
  ext
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ (F.map ε ≫ η F) ▷ F.obj A = (λ_ (F.obj A)).inv

Tactic:
by
    simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
rw [ofComonObjCoalgebraStruct_comul]
  simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
rw [ofComonObjCoalgebraStruct_comul]
  simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
⊢ Algebra.algebraMapSubmonoid S (Submonoid.powers r) ≤ IsUnit.submonoid S

Tactic:
by simpa [Submonoid.powers_le] using! hr.map (algebraMap R S)

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : n < m
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
rw [← neg_sub, ← Int.ofNat_sub h.le, selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : n < m
⊢ (algebraMap R B) (↑(Submonoid.pow x m) * 1) = (algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (α_ (X ⊗ Y) X Y).inv ≫
      (β_ X Y).hom ▷ X ▷ Y ≫
        (α_ (Y ⊗ X) X Y).hom ≫
          (α_ Y X (X ⊗ Y)).hom ≫
            Y ◁ X ◁ (β_ X Y).hom ≫
              Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 1 2 =>
    rw [← associator_inv_naturality_left]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (((((((((β_ X Y).hom ▷ (X ⊗ Y) ≫ (α_ (Y ⊗ X) X Y).inv) ≫ (α_ (Y ⊗ X) X Y).hom) ≫ (α_ Y X (X ⊗ Y)).hom) ≫
                Y ◁ X ◁ (β_ X Y).hom) ≫
              Y ◁ (α_ X Y X).inv) ≫
            Y ◁ (β_ X Y).hom ▷ X) ≫
          Y ◁ (α_ Y X X).hom) ≫
        (α_ Y Y (X ⊗ X)).inv) ≫
      (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)
Module: Mathlib.Logic.Equiv.Functor

Goal state before:
pp: α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f α
⊢ ⇑h.symm <$> ⇑h <$> x = x

Tactic:
simp [map_map]

Goal state after:
Module: Mathlib.Logic.Equiv.Functor

Goal state before:
pp: α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f β
⊢ ⇑h <$> ⇑h.symm <$> x = x

Tactic:
simp [map_map]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m) =
    FreeAbelianGroup.of (Multiplicative.ofAdd {a}) * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
FreeAbelianGroup.of_mul_of

Goal state after:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m) =
    FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (divBy s) (↑s • mk m t) = mk m t

Tactic:
divBy_apply,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (↑s • mk m t).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ = mk m t
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (End R (LocalizedModule S M))) ↑s) ((divBy s) (mk m t)) = mk m t

Tactic:
divBy_apply,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (End R (LocalizedModule S M))) ↑s) ((mk m t).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯) = mk m t
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_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)
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • lift' S g h (mk a b) = lift' S g h (r • mk a b)

Tactic:
rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.map_smul]

Goal state after:
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = ((map f).obj y).hom

Tactic:
simp only [map_obj_hom]
        rw [← Under.w u]
        simp only [map_obj_right, pushout_obj, mk_right, mk_hom]
        rw [← assoc, ← assoc, pushout.condition]

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (c.π.app j)) ((ConcreteCategory.hom (hc.lift inv_r)) (FreeCommRing.of PUnit.unit)) = inv j

Tactic:
change (hc.lift inv_r ≫ c.π.app j) (FreeCommRing.of PUnit.unit) = inv j

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (hc.lift inv_r ≫ c.π.app j)) (FreeCommRing.of PUnit.unit) = inv j
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✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.map₂ (η ◁ η✝)) ≫ 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₂ η✝)

Tactic:
rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
inst✝¹ : IsPreconnected J
inst✝ : IsPreconnected K
⊢ IsPreconnected (J × K)

Tactic:
refine .of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
inst✝¹ : IsPreconnected J
inst✝ : IsPreconnected K
a : Type (max u₁ u₂)
F : J × K ⥤ Discrete a
x✝¹ x✝ : J × K
j : J
k : K
j' : J
k' : K
⊢ F.obj (j, k) = F.obj (j', k')
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ n I x, I.FG) → FinitePresentation R A

Tactic:
rintro ⟨n, I, e, hfg⟩
    let := (FinitePresentation.mvPolynomial_aux R _).quotient hfg
    exact equiv e

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    colimit.ι (Grothendieck.ι F x✝¹.base ⋙ G) x✝¹.fiber ≫ (Grothendieck.forget F ⋙ fiberwiseColimit G).map f

Tactic:
simp only [Functor.comp_obj, Grothendieck.forget_obj, fiberwiseColimit_obj, Functor.comp_map,
      Grothendieck.forget_map, fiberwiseColimit_map, ι_colimMap_assoc, Grothendieck.ι_obj,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]
    rw [← colimit.w (Grothendieck.ι F _ ⋙ G) f.fiber]
    simp only [← Category.assoc, Functor.comp_obj, Functor.comp_map, ← G.map_comp]
    congr 2
    apply Grothendieck.ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = Y.fiber

Tactic:
subst hF; simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯

Tactic:
simp [map_map]

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := f.fiber } = f
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
W✝ : C
e : Unit → (X ⟶ W✝)
h : ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W✝
hm : ∀ (a : Unit), f ≫ m = e a
⊢ f ≫ m = e ()

Tactic:
exact hm ()

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
h : IsColimit c
⊢ IsLimit c.unop

Tactic:
exact ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
⊢ LiftableCone (F ⋙ G) H c

Tactic:
by
    refine ⟨(liftLimit ((isLimitExtendConeEquiv F (G := G ⋙ H) _).symm hc)).whisker F, ?_⟩
    let i := liftedLimitMapsToOriginal ((isLimitExtendConeEquiv F (G := G ⋙ H) _).symm hc)
    exact (Cone.whiskering F).mapIso i ≪≫ ((conesEquiv F (G ⋙ H)).unitIso.app _).symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ (F ⋙ G).Final

Tactic:
final_iff_comp_equivalence (F ⋙ G) s₃.functor,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ((F ⋙ G) ⋙ s₃.functor).Final
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
final_iff_comp_equivalence (F ⋙ G) s₃.functor,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hFG : ((F ⋙ G) ⋙ s₃.functor).Final
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
⊢ (pre X T S).Final

Tactic:
by
  refine ⟨fun f => ?_⟩
  rw [isConnected_iff_of_equivalence (StructuredArrow.preEquivalence T f)]
  exact Final.out f.right

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Zigzag (StructuredArrow.mk { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) })
    (StructuredArrow.mk { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) })

Tactic:
exact zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
    (isPreconnected_zigzag (.mk gbi) (.mk gbj))

Goal state after: