mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ x ∈ span Rₛ (⇑f '' v)

Tactic:
refine h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ f (m, s).1 ∈ ↑(span R (⇑f '' v))
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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
⊢ ∃! g', ↑R g' ∘ₗ f = ℓ ∘ₗ f

Tactic:
refine ⟨ℓ.extendScalarsOfIsLocalization S A, by simp, fun g'' h ↦ ?_⟩

Goal state after:
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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
g'' : M' →ₗ[A] Q
h : (fun g' ↦ ↑R g' ∘ₗ f = ℓ ∘ₗ f) g''
⊢ g'' = LinearMap.extendScalarsOfIsLocalization S A ℓ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.fst = prod.lift s.fst (s.snd ≫ prod.snd) ≫ prod.fst

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.snd = prod.lift s.fst (s.snd ≫ prod.snd) ≫ prod.snd

Tactic:
· simpa using h₁

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.snd = prod.lift s.fst (s.snd ≫ prod.snd) ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁✝ : PushoutCocone g₂ i₃
i₂✝ : Y₂ ⟶ t₁✝.pt
t₂✝ : PushoutCocone g₁ i₂✝
hi₂✝ : i₂✝ = t₁✝.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr

Tactic:
rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
by
  dsimp [FreeCommRing]
  rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i - 1)).IsSupported s

Tactic:
by rw [Int.cast_sub, Int.cast_one]; exact isSupported_sub hi isSupported_one

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
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 +
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T ?m.109 ?m.110 • ?m.112

Tactic:
← IsLocalization.mk'_add,

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
x y : T
m : M
s : ↥S
⊢ IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T ?m.109 ?m.110 • ?m.112
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
⊢ r • mk m s = mk n t ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • mk n t

Tactic:
| h n t =>

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
by
  with_unfolding_all
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

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
inst✝³ : Module R M
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
x : ↥T
⊢ IsUnit ((algebraMap R (End R N)) ↑x)

Tactic:
obtain ⟨m, mx⟩ := h' x
    have := IsLocalizedModule.map_units f ⟨_, mx⟩
    rw [map_mul, (Algebra.commute_algebraMap_left _ _).isUnit_mul_iff] at this
    exact this.2

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

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
subsingleton_iff_ker_eq_top S g,

Goal state after:
R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ g.ker = ⊤ ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
S : Submonoid R
⊢ Subsingleton (LocalizedModule S M)

Tactic:
IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
S : Submonoid R
⊢ ∀ (m : M), ∃ r ∈ S, r • m = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
⊢ x = y

Tactic:
by_cases hS₀ : 0 ∈ S
    · have : Subsingleton N := (IsLocalizedModule.subsingleton_iff S f).2 fun _ ↦ ⟨0, hS₀, by simp⟩
      exact Subsingleton.elim ..
    obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective S c
    obtain ⟨⟨m₁, t₁⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
    obtain ⟨⟨m₂, t₂⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
    replace hS : ∀ s ∈ S, IsRegular s := fun s hs ↦ hS s hs <| ne_of_mem_of_not_mem hs hS₀
    rw [IsLocalization.isRegular_mk' hS] at hc
    have (s : S) (x y : M) : s • x = s • y ↔ x = y := (hS _ s.2).isSMulRegular.eq_iff
    simp only [Function.uncurry_apply_pair, mk'_smul_mk', mk'_eq_mk'_iff, mul_smul, this,
      exists_const] at hxy ⊢
    simpa [smul_comm _ a, hc.isSMulRegular.eq_iff] using hxy

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
by
  simp [mapId']

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
by
  simp [mapId']

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
by
  simp [mapId']

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
hJK : J ≤ I.radical
⊢ ∃ n, J ^ n ≤ I

Tactic:
induction J, hJ using Submodule.fg_induction with

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
x : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom
        (F.map
          (Iso.refl
              (F.elementsMk
                  (op
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).left)
                  (uliftYonedaEquiv
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).hom)).fst).hom))
      (F.elementsMk
          (op
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).left)
          (uliftYonedaEquiv
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).hom)).snd =
    (unop x).snd

Tactic:
by
    dsimp
    simpa only [Functor.map_id_apply] using
      uliftYonedaEquiv.apply_symm_apply (unop x).snd

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

Goal state before:
pp: J : Type v₁
⊢ IsConnected (WidePushoutShape J)

Tactic:
by
  apply IsConnected.of_induct
  · introv hp t
    cases j
    · exact hp
    · rwa [← t (WidePushoutShape.Hom.init _)]

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
j : C
y : (F ⋙ coyoneda.obj (op d)).obj j
⊢ Nonempty (StructuredArrow d F)

Tactic:
exact ⟨StructuredArrow.mk y⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.unop.ι = c.ι

Tactic:
simp [Cofork.unop_ι, Fork.op_π]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inl f f =
    (pullback.fst f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).inv

Tactic:
← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv,

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inl f f =
    (pullback.fst f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).inv.unop.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).inv

Tactic:
← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv,

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).inv.unop.op
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
⊢ IsConnected (StructuredArrow c' (fromPUnit c))

Tactic:
let : Inhabited (StructuredArrow c' (fromPUnit c)) := ⟨.mk (Y := default) (hc.from c')⟩
    let : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
      ⟨fun i j ↦ StructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩
    infer_instance

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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ RingHom.ker f.toRingHom = Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom)

Tactic:
simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]

Goal state after:
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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ((↑f).comp ↑g) ⊥)
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.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ =
    pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)

Tactic:
trans l₁' ≫ pullback.fst _ _

Goal state after:
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.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ =
    pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫
      pullback.fst f₁ f₂

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₂)
⊢ pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫
      pullback.fst f₁ f₂ =
    pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (Cofork.ofπ h ⋯)

Tactic:
by
    apply Cofork.IsColimit.mk' _ _
    intro s
    have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by
      rw [← Category.assoc, ← Category.assoc, s.condition]
    obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) l₁
    obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.symm
    refine ⟨p, hp₁, ?_⟩
    intro m w
    have z := w.trans hp₁.symm
    apply t.hom_ext
    have := gr.epi
    apply (PushoutCocone.mk _ _ comm).coequalizer_ext
    · exact z
    · erw [← cancel_epi g, ← Category.assoc, ← eq_whisker comm]
      erw [← Category.assoc, ← eq_whisker comm]
      dsimp at z; simp only [Category.assoc, z]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g], P g → ∃ T fst snd, IsPullback fst snd f g ∧ P fst
⊢ P.IsStableUnderBaseChange

Tactic:
refine .mk' fun X Y S f g _ hg ↦ ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g], P g → ∃ T fst snd, IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : P g
⊢ P (pullback.fst f g)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g], P f → ∃ T inl inr, IsPushout f g inl inr ∧ P inr
⊢ P.IsStableUnderCobaseChange

Tactic:
refine .mk' fun X Y S f g _ hg ↦ ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g], P f → ∃ T inl inr, IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
x✝ : HasPushout f g
hg : P f
⊢ P (pushout.inr f g)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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 X ⊗ₘ fst Y Z

Tactic:
ext <;> simp [tensorμ]

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

Goal state before:
pp: 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 W X ⊗ₘ snd Y Z

Tactic:
ext <;> simp [tensorμ]

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

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ (((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft
            (Functor.Monoidal.commTensorLeft F X).compInverseIso).homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
Adjunction.homEquiv_ofNatIsoLeft_apply

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙.hom

Tactic:
by
  convert! coevaluation_evaluation X Y <;> simp [monoidalComp]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
have hr : Module.rank R f'.range ≤ Module.rank R p := by grw [Submodule.rank_le f'.range]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := f.restrict ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
rw [lift_umax.{u, v}, lift_id'.{u, v}] at this

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)