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

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ ↑⟨inrHom R' N ∘ₗ f, ⋯⟩ x = inr (f x)

Tactic:
LinearMap.comp_apply,

Goal state after:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ (inrHom R' N) (f x) = inr (f x)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul ∘ₗ comul =
    lTensor (ι →₀ A) comul ∘ₗ comul

Tactic:
by
    ext i : 1
    simp_rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, comul_comp_lsingle,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_lsingle, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq]

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
⊢ map' f (𝟙 M) = 𝟙 (obj' f M)

Tactic:
simp [map', obj']

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

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [comul_def, coassoc_simps]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.counit) =
    ModuleCat.Hom.hom (ρ_ (ModuleCat.of R ↑X.toModuleCat)).inv

Tactic:
simpa using! Coalgebra.lTensor_counit_comp_comul

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
⊢ Monotone fun I ↦ { ringCon := I.ringCon.comap f }

Tactic:
by
    intro I J h
    rw [le_iff] at h
    intro x
    specialize @h (f x)
    simpa [mem_iff, RingCon.comap]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * (y * x + 1) - 1 ∈ I

Tactic:
hr,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ q - 1 ∈ I
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)

Tactic:
intro b
    obtain ⟨a, rfl⟩ := hf b
    apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
    rw [← f.map_one, ← f.map_sub]
    apply f.isUnit_map

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rw [selfZPow_of_neg _ _ hn, selfZPow_of_neg _ _ hm, selfZPow_of_neg _ _ (add_neg hn hm),
      Int.natAbs_add_of_nonpos hn.le hm.le, ← mk'_mul, one_mul]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) = mk' B 1 (Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

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
x : R
s : ↥S
⊢ s • mk' A x s = (Algebra.linearMap R A) x

Tactic:
exact IsLocalization.smul_mk'_self

Goal state after:
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
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : s • ∑ i ∈ t, fg (Sum.inl i) • v i = s • ∑ i ∈ t, fg (Sum.inr i) • v i
⊢ g₁ i = g₂ i

Tactic:
simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at eq

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
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : ∑ x ∈ t, (↑s * fg (Sum.inl x)) • v x = ∑ x ∈ t, (↑s * fg (Sum.inr x)) • v x
⊢ g₁ i = g₂ i
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
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ (ofIsLocalizedModule Rₛ S f b).repr ((ofIsLocalizedModule Rₛ S f b) i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)

Tactic:
repr_self,

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
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)
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
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (b.repr (b i))

Tactic:
repr_self,

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
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ Finsupp.single i 1 = (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (Finsupp.single i 1)
Module: Mathlib.RingTheory.Localization.Module

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.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ (mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm = LinearMap.id

Tactic:
apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.linearMap_ext S g g
      ext; simp

Goal state after:
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'
h : IsBaseChange A f
this : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
⊢ IsLocalizedModule S f

Tactic:
have : IsBaseChange A (LocalizedModule.mkLinearMap S M) := IsLocalizedModule.isBaseChange S A _

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'
h : IsBaseChange A f
this✝ : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange A (LocalizedModule.mkLinearMap S M)
⊢ IsLocalizedModule S f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z Z' : C
f : Z ⟶ X
g : Z' ⟶ Y
i : Z' ⟶ Z
inst✝ : IsIso i
h : HasPushout f (inv i ≫ g)
⊢ HasPushout (i ≫ f) g

Tactic:
simpa using hasPushout_of_epi_comp f (inv i ≫ g) i

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'
s : ↥S
r : R
x : LocalizedModule S M
x✝¹ : M
x✝ : ↥S
⊢ (r • mk x✝¹ x✝).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (RingHom.id R) r • (mk x✝¹ x✝).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
simp_rw [smul'_mk, liftOn_mk, smul'_mk]

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
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
r : R
x : LocalizedModule S M
x✝¹ : M
x✝ : ↥S
⊢ mk (r • x✝¹) (x✝ * s) = mk ((RingHom.id R) r • x✝¹) (x✝ * s)
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
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)

Tactic:
fromLocalizedModule'_mk,

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
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (f a) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)
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
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (f a) = fromLocalizedModule' S f (LocalizedModule.mk (r • a) b)

Tactic:
fromLocalizedModule'_mk,

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
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f (r • a))
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right

Goal state after:
case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv
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
⊢ (↑(iso S f).symm ∘ₗ f) m = (LocalizedModule.mkLinearMap S M) m

Tactic:
LinearMap.comp_apply,

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
⊢ ↑(iso S f).symm (f m) = (LocalizedModule.mkLinearMap S M) m
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right

Goal state after:
case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
x✝ y✝ : M
hxy : g (f x✝) = g (f y✝)
⊢ f x✝ - f y✝ = 0

Tactic:
← map_sub

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
x✝ y✝ : M
hxy : g (f x✝) = g (f y✝)
⊢ f (x✝ - y✝) = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
exact ⟨Q.strictMap F, inferInstance, (map_monotone h₂ F).trans (by simp)⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG

Tactic:
let g : t → AX := fun x => MvPolynomial.C (x : A) - map (algebraMap R A) (t' x)

Goal state after:
case refine_2
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.unop.left.op)) ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩.snd =
    ⟨op (unop Y).left, yonedaEquiv.toFun (unop Y).hom⟩.snd

Tactic:
simp [yonedaEquiv_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
w_fiber : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base✝ : X.base ⟶ Y.base
fiber✝ : (F.map base✝).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base✝, fiber := fiber✝ }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match of X with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

Goal state after:
case of.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
⊢ G.map PUnit.unit ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match of X with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      (match of Y with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f

Goal state after: