mathlib-initiative/mathlib-tactics huggingface dataset:
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
a✝ : Π₀ (j : J), ↑((F ⋙ uliftFunctor).obj j)
hx :
  a✝ ∈
    {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
obtain ⟨j, j', u, a, rfl⟩ := hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a ∈
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom = (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ X₁ X₂ (𝟙_ C) (𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom)

Tactic:
by
  dsimp only [tensorμ]
  have :
    ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
        (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
      (α_ X₁ X₂ (𝟙_ C)).hom ≫ (X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) := by
    monoidal
  slice_rhs 1 3 => rw [this]
  clear this
  slice_rhs 2 3 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    rightUnitor_inv_braiding]
  simp [tensorHom_def]

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₂
X✝ : D
⊢ ((fun α ↦
              TwoSquare.mk R₁ H G R₂
                ((R₁ ⋙ G).rightUnitor.inv ≫
                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
            ((fun β ↦
                TwoSquare.mk G L₁ L₂ H
                  ((G ⋙ L₂).leftUnitor.inv ≫
                    whiskerRight adj₁.unit (G ⋙ L₂) ≫
                      ((L₁ ⋙ R₁).associator G L₂).inv ≫
                        whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                          whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                            whiskerRight (L₁.associator H R₂).inv L₂ ≫
                              ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                                (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
              β)).natTrans.app
      X✝ =
    β.natTrans.app X✝

Tactic:
simp only [comp_obj, whiskerRight_comp, whiskerRight_twice, assoc, Iso.inv_hom_id_assoc,
      whiskerLeft_comp, comp_app, id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app,
      associator_hom_app, associator_inv_app, Functor.whiskerRight_app, leftUnitor_inv_app, map_id,
      Functor.comp_map, rightUnitor_hom_app, leftUnitor_hom_app, comp_id, id_comp,
      unit_naturality_assoc, right_triangle_components_assoc]

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₂
X✝ : D
⊢ G.map (adj₁.unit.app (R₁.obj X✝)) ≫ β.natTrans.app (L₁.obj (R₁.obj X✝)) ≫ R₂.map (H.map (adj₁.counit.app X✝)) =
    β.natTrans.app X✝
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring M
inst✝² : Algebra R M
inst✝¹ : Semiring P
inst✝ : Algebra R P
f : M →ₐ[R] P
x : M
⊢ (kerLiftₐ f) ↑x = f x

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring M
inst✝² : Algebra R M
inst✝¹ : Semiring P
inst✝ : Algebra R P
f : M →ₐ[R] P
x : M
⊢ ↑((quotientKerEquivRangeₐ f) ↑x) = f x

Tactic:
by
  rfl

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

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : { f // ∀ (x y : M), f x * f y = 0 }
r : R'
x : M
⊢ (Algebra.ofId R' A, ↑f).2 (r •> x) = (Algebra.ofId R' A, ↑f).1 r * (Algebra.ofId R' A, ↑f).2 x

Tactic:
by simp [Algebra.smul_def, Algebra.ofId_apply]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₗc[R] B
h : f.toFun 1 = 1
h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y
⊢ ↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : CoalgebraStruct R A
inst✝ : CoalgebraStruct R B
f : A →ₐc[R] B
⊢ ↑↑f = ↑f

Tactic:
by
  rfl

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

Goal state before:
pp: R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M))
          ((extendScalarsComp f₁₂ f₂₃).hom.app M)))
      m =
    1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)

Tactic:
homEquiv_extendScalarsComp

Goal state after:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        ((extendRestrictScalarsAdj f₁₂).unit.app M ≫
          (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
            (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))))
      m =
    1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
by
  simp [leftAdjointUniq]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

Tactic:
by
  simp [leftAdjointUniq]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.leftAdjointUniq adj1).hom = 𝟙 F

Tactic:
by
  simp [leftAdjointUniq]

Goal state after:
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X✝ Y✝ Z✝ : Preord
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization =
    PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization

Tactic:
ext x
    induction x using Quotient.inductionOn'
    exact OrderHom.antisymmetrization_apply_mk ..

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
A B : C
inst✝¹ : ComonObj A
inst✝ : ComonObj B
⊢ Δ = (Δ ⊗ₘ Δ) ≫ (tensorμ (op A) (op B) (op A) (op B)).unop

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I✝ I : TwoSidedIdeal R
a✝ x✝ : R
⊢ a✝ ∈ asIdeal I → a✝ * x✝ ∈ asIdeal I

Tactic:
simpa using I.mul_mem_right _ _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
by
  have mem := (Ideal.eq_top_iff_one _).mp span_eq; clear span_eq
  wlog finset_eq : ∃ t : Finset R, t = s generalizing s
  · have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span mem
    have ⟨r, eq, uniq⟩ := this t (fun a ↦ f ⟨a, hts a.2⟩)
      (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) mem ⟨_, rfl⟩
    refine ⟨r, fun a ↦ ?_, fun _ eq ↦ uniq _ fun a ↦ eq ⟨a, hts a.2⟩⟩
    replace hts := Set.insert_subset a.2 hts
    classical
    have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩
    exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)
  have span_eq := (Ideal.eq_top_iff_one _).mpr mem
  refine existsUnique_of_exists_of_unique ?_ fun x y hx hy ↦
    algebraMap_injective_of_span_eq_top s span_eq (funext fun a ↦ (hx a).trans (hy a).symm)
  obtain ⟨s, rfl⟩ := finset_eq
  choose n r eq using fun a ↦ Away.surj a.1 (f a)
  let N := s.attach.sup n
  let r a := a ^ (N - n a) * r a
  have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
      Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]
  have eq2 a b : ∃ N', (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) :=
    Away.exists_of_eq (S := Away (a * b : R)) _ <| by
      simp_rw [map_mul, ← Away.awayToAwayRight_eq (S := Away a.1) a.1 b (r a),
        ← Away.awayToAwayLeft_eq (S := Away b.1) b.1 a (r b), ← eq, map_mul,
        Away.awayToAwayRight_eq, Away.awayToAwayLeft_eq, h, mul_assoc, ← map_mul, mul_comm]
  choose N' hN' using eq2
  let N' := (s ×ˢ s).attach.sup fun a ↦ N'
    ⟨_, (Finset.mem_product.mp a.2).1⟩ ⟨_, (Finset.mem_product.mp a.2).2⟩
  have eq2 a b : (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) := by
    dsimp only [N']; rw [← Nat.sub_add_cancel (Finset.le_sup <| (Finset.mem_attach _ ⟨⟨a, b⟩,
      Finset.mk_mem_product a.2 b.2⟩)), pow_add, mul_assoc, hN', ← mul_assoc]
  let N := N' + N
  let r a := a ^ N' * r a
  have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_mul, ← pow_add]
  have eq2 a b : r a * b ^ N = r b * a ^ N := by
    rw [pow_add, mul_mul_mul_comm, ← mul_pow, eq2,
      mul_comm a.1, mul_pow, mul_mul_mul_comm, ← pow_add]
  have ⟨c, eq1⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp <|
    (Ideal.eq_top_iff_one _).mp <| (Set.image_eq_range _ _ ▸ Ideal.span_pow_eq_top _ span_eq N)
  refine ⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩
  simp_rw [← map_pow, eq, ← map_mul, Finset.sum_mul, mul_assoc, eq2 _ a, mul_left_comm (c _),
    ← Finset.mul_sum, ← smul_eq_mul (a := c _), eq1, mul_one]

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)

Tactic:
let : Algebra A (S ⊗[R] B) := .compHom _ (algebraMap A B)

Goal state after:
R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: 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✝
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
r : R
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map Algebra.TensorProduct.includeRight M
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
⊢ ∀ (x : S), (algebraMap S (S ⊗[R] B)) x = (algebraMap (S ⊗[R] A) (S ⊗[R] B)) ((algebraMap S (S ⊗[R] A)) x)

Tactic:
intro; simp [RingHom.algebraMap_toAlgebra]

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
r : R
m : M
s s' : ↥S
⊢ IsLocalization.mk' T r s • mk m s' = mk (r • m) (s * s')

Tactic:
rw [smul_def, mk_eq]

Goal state after:
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
r : R
m : M
s s' : ↥S
⊢ ∃ u,
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • 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
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:
by
    induction p with | _ m s
    rw [← IsLocalization.mk'_sec (M := S) T x, IsLocalization.smul_mk', mk'_smul_mk, mk'_smul_mk,
      smul'_mk, mul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
y : N
x : M
r : R
hr₁ : r ∈ ↑S
hx : (x, ⟨(algebraMap R A) r, ⋯⟩).2 • y = f (x, ⟨(algebraMap R A) r, ⋯⟩).1
⊢ (x, ⟨r, hr₁⟩).2 • y = (↑R f) (x, ⟨r, hr₁⟩).1

Tactic:
simpa [Submonoid.smul_def] using hx

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

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤

Tactic:
by
  algebraize [f.hom, g.hom]
  let e := ((isPushout_tensorProduct R A B).isoIsPushout A B H).commRingCatIsoToRingEquiv
  rw [← Subring.comap_map_eq_self_of_injective e.symm.injective (.closure _), RingHom.map_closure,
    ← top_le_iff, ← Subring.map_le_iff_le_comap, Set.image_union]
  simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]
  rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv,
    hom_ofHom, hom_ofHom]
  exact le_top.trans (Algebra.TensorProduct.closure_range_union_range_eq_top R A B).ge

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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l ↦ l ∘ₗ f = f) y → y = e
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
← toLinearMap_inj,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left✝ : e ∘ₗ f = f
univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l ↦ l ∘ₗ f = f) y → y = e
⊢ ↑(iso S (mkLinearMap S M)) = ↑(LinearEquiv.refl R (LocalizedModule S M))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
⊢ ↑((ConcreteCategory.hom m) x) = ((Hom.hom s.fst) x, (Hom.hom s.snd) x)

Tactic:
have eq2 := (congr_arg (fun f : s.pt →+* B => f x) (congrArg Hom.hom e₂) :)

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) = ((Hom.hom s.fst) x, (Hom.hom s.snd) x)
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type (max v u)
j : J
⊢ ((productIso F).hom ≫ ↾fun f ↦ f j) = Pi.π F j

Tactic:
by
  rfl

Goal state after:
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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
this : RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG

Tactic:
by
    rw [this]
    exact hf.2

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ (F ⋙ G).map g ≫ c.ι.app Z₂

Tactic:
c.w,

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) =
    (G.map (homToLift F X) ≫ c.ι.app (lift F X)) ≫ ((const D).obj c.pt).map f

Tactic:
dsimp; simp only [Category.comp_id]
            -- This would be true if we'd chosen `lift F X` to be `lift F Y`
            -- and `homToLift F X` to be `f ≫ homToLift F Y`.
            apply
              induction F fun Z k =>
                G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k ≫ c.ι.app Z
            · intro Z₁ Z₂ k₁ k₂ g a z
              rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]
            · intro Z₁ Z₂ k₁ k₂ g a z
              rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w] at z
              rw [z]
            · rw [← Functor.map_comp_assoc]

Goal state after: