mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ mk ((IsLocalization.sec S t).1 • (IsLocalization.sec S t').1 • m)
      ((IsLocalization.sec S t).2 * ((IsLocalization.sec S t').2 * s)) =
    mk ((IsLocalization.sec S t').1 • (IsLocalization.sec S t).1 • m)
      ((IsLocalization.sec S t').2 * ((IsLocalization.sec S t).2 * s))

Tactic:
smul_smul,

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ mk (((IsLocalization.sec S t).1 * (IsLocalization.sec S t').1) • m)
      ((IsLocalization.sec S t).2 * ((IsLocalization.sec S t').2 * s)) =
    mk (((IsLocalization.sec S t').1 * (IsLocalization.sec S t).1) • m)
      ((IsLocalization.sec S t').2 * ((IsLocalization.sec S t).2 * s))
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 1 • p = p

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 • mk m s = mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ mk (1 • m) (1 * s) = mk m s

Tactic:
one_smul,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ mk m (1 * s) = mk m s
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
p : LocalizedModule S M
⊢ (x * y) • p = x • y • p

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x * y) • mk m s = x • y • mk m s
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
p q : LocalizedModule S M
⊢ x • (p + q) = x • p + x • q

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
q : LocalizedModule S M
m : M
s : ↥S
⊢ x • (mk m s + q) = x • mk m s + x • q
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
p : LocalizedModule S M
⊢ (x + y) • p = x • p + y • p

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (x + y) • mk m s = x • mk m s + y • mk m s
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 0 • p = 0

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 0 • mk m s = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ mk (r • m) s = mk n t ↔ mk m s = mk (1 • n) (⟨r, hr⟩ * t)

Tactic:
one_smul,

Goal state after:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ mk (r • m) s = mk n t ↔ mk m s = mk n (⟨r, hr⟩ * 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
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
p : LocalizedModule S M
⊢ (r • x) • p = r • x • p

Tactic:
induction p with | _ m s

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ (r • x) • mk m s = r • x • mk m s
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
N : Type u_2
inst✝ : Monoid N
f g : M →* N
r : M
hr : f r = g r
⊢ IsUnit ⟨r, hr⟩ ↔ IsUnit r

Tactic:
refine ⟨fun h ↦ h.map (SubmonoidClass.subtype _), fun h ↦ ?_⟩
  obtain ⟨s, hs⟩ := isUnit_iff_exists.mp h
  suffices ∃ a, r * a = 1 ∧ f a = g a ∧ a * r = 1 by
    simpa [isUnit_iff_exists, ← Subtype.val_inj]
  refine ⟨s, hs.left, ?_, hs.right⟩
  rw [← mul_one (f s), ← map_one g, ← hs.left, map_mul, ← mul_assoc, ← hr, ← map_mul,
    hs.right, map_one, one_mul]

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''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
f : M →ₗ[R] M'
e : M' →ₗ[R] M''
he : Function.Bijective ⇑e
h : IsLocalizedModule S (e ∘ₗ f)
this : ↑(LinearEquiv.ofBijective e he).symm ∘ₗ e ∘ₗ f = f
⊢ IsLocalizedModule S (↑(LinearEquiv.ofBijective e he).symm ∘ₗ e ∘ₗ f)

Tactic:
exact .of_linearEquiv _ _ _

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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (∃ s, 0 = s • 1 • m) ↔ ∃ s', s' • m = 0

Tactic:
one_smul,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (∃ s, 0 = s • m) ↔ ∃ s', s' • m = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
← small_op_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P.unop.op ↔ ObjectProperty.Small.{w, v, u} P
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber

Tactic:
· dsimp [comp, id]
      rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]
      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 G : C ⥤ Cat
α : F ⟶ G
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ { base := (f ≫ g).base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Z.base).toFunctor.map (f ≫ g).fiber } =
    { base := f.base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Y.base).toFunctor.map f.fiber } ≫
      { base := g.base, fiber := (eqToHom ⋯).toNatTrans.app Y.fiber ≫ (α.app Z.base).toFunctor.map g.fiber }

Tactic:
apply Grothendieck.ext _ _ (by simp)
    simp only [comp_fiber, map_comp, ← Cat.Hom.comp_map,
      Functor.congr_hom congr($(α.naturality g.base).toFunctor) f.fiber]
    simp

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✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Tactic:
let hc' := isLimitOfPreserves H ((isLimitWhiskerEquiv F _).symm hc)

Goal state after:
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✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ IsLimit (Cone.whisker F (H.mapCone c))
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 (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone (liftLimit ((isLimitWhiskerEquiv F c).symm hc)) ≅ Cone.whisker F c :=
  liftedLimitMapsToOriginal ((isLimitWhiskerEquiv F c).symm hc)
⊢ H.mapCone (extendCone.obj (liftLimit ((isLimitWhiskerEquiv F c).symm hc))) ≅
    extendCone.obj (H.mapCone (liftLimit ((isLimitWhiskerEquiv F c).symm hc)))

Tactic:
exact Cone.ext (Iso.refl _)

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

Goal state before:
pp: case refine_2
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯ ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
⊢ (Cone.postcompose
          (NatIso.ofComponents
              (fun k ↦
                Over.isoMk
                  (Iso.refl
                    ((Over.lift (Over.forget j ⋙ D)
                            (Functor.whiskerRight (Over.forgetCocone j).ι D ≫
                              (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)).obj
                        k).left)
                  ⋯)
              ⋯).hom).obj
      c'' ≅
    c.overPost j

Tactic:
exact Cone.ext (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄

Tactic:
by
  rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
⊢ P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)

Tactic:
let e₁ : R' ≃+* Localization.Away r :=
    (IsLocalization.algEquiv (Submonoid.powers r) _ _).toRingEquiv
  let e₂ : Localization.Away (f r) ≃+* S' :=
    (IsLocalization.algEquiv (Submonoid.powers (f r)) _ _).toRingEquiv
  refine (hP.cancel_left_isIso e₁.toCommRingCatIso.hom (CommRingCat.ofHom _)).symm.trans ?_
  refine (hP.cancel_right_isIso (CommRingCat.ofHom _) e₂.toCommRingCatIso.hom).symm.trans ?_
  rw [← eq_iff_iff]
  congr 1
  -- Porting note: Here, the proof used to have a huge `simp` involving `[anonymous]`, which didn't
  -- work out anymore. The issue seemed to be that it couldn't handle a term in which Ring
  -- homomorphisms were repeatedly casted to the bundled category and back. Here we resolve the
  -- problem by converting the goal to a more straightforward form.
  let e := (e₂ : Localization.Away (f r) →+* S').comp
      (((IsLocalization.map (Localization.Away (f r)) f
            (by rintro x ⟨n, rfl⟩; use n; simp : Submonoid.powers r ≤ Submonoid.comap f
                (Submonoid.powers (f r)))) : Localization.Away r →+* Localization.Away (f r)).comp
                (e₁ : R' →+* Localization.Away r))
  suffices e = IsLocalization.Away.map R' S' f r by
    convert! this
  apply IsLocalization.ringHom_ext (Submonoid.powers r) _
  ext1 x
  dsimp [e, e₁, e₂, IsLocalization.Away.map]
  simp only [IsLocalization.map_eq, id_apply, RingHomCompTriple.comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
⊢ m ≫ c₂.fst = s.π.app { as := 0 }

Tactic:
apply w ⟨0⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })

Tactic:
have fac : e₁.hom ≫ g = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) ≫ e₂.hom := e.hom.w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inl ≫ m = s.ι.app { as := 0 }

Tactic:
apply w ⟨0⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone coproducts.{w, v, u}

Tactic:
rintro W₁ W₂ h X Y f hf
  rw [coproducts_iff] at hf
  obtain ⟨J, hf⟩ := hf
  exact W₂.colimitsOfShape_le_coproducts J _
    (colimitsOfShape_monotone h _ _ hf)

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
⊢ ∀ (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (e.hom ≫ f) → P f'

Tactic:
f'

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
⊢ IsPullback f' i₁ i₂ (e.hom ≫ f) → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
⊢ ∀ (f' : X' ⟶ Z'), IsPullback f' i₁ i₂ (f ≫ e.hom) → P f'

Tactic:
f'

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
⊢ IsPullback f' i₁ i₂ (f ≫ e.hom) → P f'
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ fst W Y = (fst W X ⊗ₘ fst Y Z) ≫ fst W Y

Tactic:
simp [tensorμ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z)) ≫ snd W Y = (fst W X ⊗ₘ fst Y Z) ≫ snd W Y

Tactic:
simp [tensorμ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ fst X Z = (snd W X ⊗ₘ snd Y Z) ≫ fst X Z

Tactic:
simp [tensorμ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (toUnit (𝟙_ C) ≫ η) = toUnit (𝟙_ C) ≫ η

Tactic:
exact (α.app _).hom.map_one

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z)) ≫ snd X Z = (snd W X ⊗ₘ snd Y Z) ≫ snd X Z

Tactic:
simp [tensorμ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
⊢ h ≫ f ^ 0 = (h ≫ f) ^ 0

Tactic:
simp [pow_succ, MonObj.comp_mul, *]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
h : Y ⟶ X
n✝ : ℕ
a✝ : h ≫ f ^ n✝ = (h ≫ f) ^ n✝
⊢ h ≫ f ^ (n✝ + 1) = (h ≫ f) ^ (n✝ + 1)

Tactic:
simp [pow_succ, MonObj.comp_mul, *]

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op = (λ_ (op (of R A))).hom

Tactic:
by ext; exact Coalgebra.rTensor_counit_comul _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    (Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)))) (x ⊗ₜ[R] y) =
      (Hom.hom
          (↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
              (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))))
        (x ⊗ₜ[R] y)

Tactic:
apply monoidalClosed_uncurry

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.toDual x) (b i) = (b.toDual y) (b i)

Tactic:
exact DFunLike.congr_fun h _

Goal state after: