mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (bifunctorComp₁₂ F₁₂ G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      (bifunctorComp₁₂ F₁₂ G').map f

Tactic:
ext X₂ X₃
        dsimp
        simp only [← NatTrans.comp_app, NatTrans.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₂₃FunctorObj F).obj G₂₃).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₂₃FunctorObj F').obj G₂₃).map f

Tactic:
ext X₂ X₃
        dsimp
        simp only [← NatTrans.comp_app, NatTrans.naturality]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z)

Tactic:
rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv = (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z

Tactic:
rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ G.obj Z) ≫
          δ F (G.obj (X ⊗ Y)) (G.obj Z) ≫ (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
rw [← δ_natural_left_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : isomorphisms C f
hg : isomorphisms C g
⊢ isomorphisms C (f ≫ g)

Tactic:
rw [isomorphisms.iff] at hf hg ⊢
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)

Tactic:
apply epi_comp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.op g.op ↔ HasPushout f g

Tactic:
by
  rw [HasPullback, hasLimit_iff_of_iso (cospanOp f g), hasLimit_inverse_equivalence_comp_iff,
    hasLimit_op_iff_hasColimit]

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
x : Quot F
j : J
a : ↑(F.obj j)
⊢ (quotUliftToQuot F) ((quotToQuotUlift F) ((Quot.ι F j) a)) = (Quot.ι F j) a

Tactic:
quotToQuotUlift_ι,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ (quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) { down := a }) = (Quot.ι F j) a
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
| L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d)

Tactic:
rw [← (mateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
| L₂.map (((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app (H.obj d)
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
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) = (Quot.desc F s) x

Tactic:
suffices eq : m.hom.comp (AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s by
      rw [← eq]; rfl

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ f ≫ ofHom (mk' (Hom.hom f).range) = 0

Tactic:
by
        ext x
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
| G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c)

Tactic:
rw [← (mateEquiv adj₁ adj₂).right_inv α]

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
| G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
⊢ ∀ (a₁ a₂ : M), c.toSetoid a₁ a₂ ↔ d.toSetoid (↑e a₁) (↑e a₂)

Tactic:
apply RingCon.ext_iff.mp h

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ (forget₂ RingCat AddCommGrpCat).IsRightAdjoint

Tactic:
by
  rw [← Functor.isRightAdjoint_comp_iff_right (forget₂ (AlgCat.{u} ℤ) RingCat.{u})]
  have heq : forget₂ (AlgCat.{u} ℤ) _ ⋙ forget₂ (ModuleCat.{u} ℤ) AddCommGrpCat.{u} =
      forget₂ (AlgCat.{u} ℤ) RingCat.{u} ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u} :=
    rfl
  rw [← heq]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β

Tactic:
simp only [Equiv.apply_symm_apply]

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
inst✝² : MonoidalCategory C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ 𝟙 (𝟙_ C) = (ρ_ (𝟙_ C)).inv

Tactic:
by monoidal_coherence

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
inst✝² : MonoidalCategory C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv = (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom

Tactic:
by monoidal_coherence

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a

Tactic:
obtain ⟨a, ⟨n, rfl⟩, hm⟩ := wellFounded_dvdNotUnit.has_min
    {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ∃ n_1 a_1, ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ asIdeal J
x : R
hx : x ∈ fromIdeal I
⊢ x ∈ J

Tactic:
by
    simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx
    exact hx _ h

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * a) → IsUnit a

R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * b) → IsUnit b
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
⊢ I ⨯ X ≅ I

Tactic:
have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
this : IsIso prod.fst
⊢ I ⨯ X ≅ I
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
⊢ 𝟙_ C ◁ 𝟙 (𝟙_ C) ≫ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
by monoidal_coherence

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
⊢ (λ_ (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom

Tactic:
by monoidal_coherence

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ (↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ ↑(IsLocalizedModule.iso S g₁).symm =
    (IsLocalizedModule.map S g₁ g₂) l

Tactic:
apply IsLocalizedModule.linearMap_ext S g₁ g₂

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ((↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ ↑(IsLocalizedModule.iso S g₁).symm) ∘ₗ g₁ =
    (IsLocalizedModule.map S g₁ g₂) l ∘ₗ g₁
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: case neg
R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
h : ¬a = b
⊢ 0 = e (1 ⊗ₜ[R] 0)

Tactic:
simp only [tmul_zero, map_zero]

Goal state after:
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'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a : A
s : ↥S
⊢ 1 • 1 • ((0, 1).1 * (a, s).1) = 1 • ((a, s).2 * (0, 1).2) • 0

Tactic:
by simp only [zero_mul, smul_zero]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompl F G H)

Tactic:
by
  constructor <;> intros <;> simp [bimap, map_id, map_comp_map, functor_norm]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : α → R
F : Multiplicative (Multiset α) →* R
x : Multiplicative (Multiset α)
F' : Multiset α →+ Additive R := MonoidHom.toAdditiveRight F
x' : Multiset α := Multiplicative.toAdd x
⊢ F' (Multiset.map (fun x ↦ {x}) x').sum = F' x'

Tactic:
exact DFunLike.congr_arg F (Multiset.sum_map_singleton x')

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : Nonempty (IsLimit (BinaryFan.mk fst snd))
⊢ IsPullback fst snd f g

Tactic:
· exact ⟨⟨by subsingleton⟩,
      ⟨PullbackCone.IsLimit.mk _ (fun s ↦ BinaryFan.IsLimit.lift h.some s.fst s.snd)
      (by subsingleton) (by subsingleton) (by subsingleton)⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.η.app X ≫ T.map f ≫ Y.a = f

Tactic:
← T.η.naturality_assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ (𝟭 C).map f ≫ T.η.app Y.A ≫ Y.a = f
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), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
⊢ (fun g ↦ (terminal.from (CostructuredArrow.mk g)).left) ((fun g ↦ G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g

Tactic:
by
    let B' : CostructuredArrow G A :=
      CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
    let g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g rfl
    have : terminal.from _ = g' := by cat_disch
    change CommaMorphism.left (terminal.from B') = _
    rw [this]
    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
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
⊢ a = b

Tactic:
obtain ⟨⟨y, n⟩, (hym : n • b = f y)⟩ := IsLocalizedModule.surj S f b

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
⊢ a = b
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map f = F.map g

Tactic:
by rw [← hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1
X : Type u
⊢ binaryProductFunctor.obj X ≅ prod.functor.obj X

Tactic:
refine NatIso.ofComponents (fun Y => ?_) (fun _ => ?_)

Goal state after:
case refine_1.refine_1
X Y : Type u
⊢ (binaryProductFunctor.obj X).obj Y ≅ (prod.functor.obj X).obj Y

case refine_1.refine_2
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫ Iso.hom ?refine_1.refine_1 =
    Iso.hom ?refine_1.refine_1 ≫ (prod.functor.obj X).map x✝
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
⊢ FinitePresentation R B

Tactic:
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
  use n, AlgHom.comp (↑e) f
  constructor
  · rw [AlgHom.coe_comp]
    exact Function.Surjective.comp e.surjective hf.1
  suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom by
    rw [this]
    exact hf.2
  have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
    f.toRingHom := by
    have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
    have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
    rw [h, h1]
  rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P.op
    exact ⟨Q.unop, inferInstance, by rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]⟩

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

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ : a✝¹ ⟶ b✝
a✝ : ↑a✝¹
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app (of a✝) =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      (of a✝)

pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star

Tactic:
· simpa using! (refl _)

Goal state after:
case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star
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
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ (pre F G.functor).map
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            (𝟙
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                    pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)

Tactic:
fapply Grothendieck.ext <;> simp [preNatIso, transportIso]

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

Goal state before:
pp: 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
⊢ c.op.unop.π ≫ (Iso.refl c.op.unop.pt).hom = c.π

Tactic:
simp [op_unop_π]

Goal state after: