mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₂'.Exact

Tactic:
← exact_op_iff,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₂'.op.Exact
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'

Tactic:
rw [α.hom.naturality f']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
by rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse (Sum.elim left right) fun x ↦
    match x with
    | left a => Sum.inl a
    | right b => Sum.inr b

Tactic:
by rintro (_ | _) <;> rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
this :
  Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f) ∧
    Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
⊢ Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)

Tactic:
exact this.1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
c : Fan I.left
d : Fan I.right
hd : IsLimit d
i : J.R
⊢ I.fstPiMapOfIsLimit c hd ≫ d.proj i = c.proj (J.fst i) ≫ I.fst i

Tactic:
simp [fstPiMapOfIsLimit]

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

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv).range = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv).ker

Tactic:
by simp [LinearMap.range_comp, LinearMap.ker_comp, exac, Submodule.comap_equiv_eq_map_symm]

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

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv).range = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv).ker

Tactic:
by simp [LinearMap.range_comp, LinearMap.ker_comp, exac, Submodule.comap_equiv_eq_map_symm]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
i j : ℕ
hij : i ≤ j
hjn : j ≤ n
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]; valid

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

Goal state before:
pp: case zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫
      (reflectorAdjunction R).unit.app (R.obj ((reflector R).obj X.A)) ≫
        R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A

Tactic:
Adjunction.right_triangle_components,

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app X.A ≫ 𝟙 (R.obj ((reflector R).obj X.A)) =
    (reflectorAdjunction R).unit.app X.A ≫ X.a ≫ (reflectorAdjunction R).unit.app X.A
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk

Tactic:
simp [Fin.ext_iff] at hjk

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B)

Tactic:
apply equalizer.hom_ext
  change
    equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ =
      equalizer.lift _ _ ≫ equalizer.ι _ _
  simp [Adjunction.homEquiv_unit]

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ IsBaseChange Rp ?m.51

pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ M →ₗ[R] Mp

Tactic:
exact (isLocalizedModule_iff_isBaseChange S Rp f).mp h

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x ↦ (a + b) • x) x ∈ a • s + b • s
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ J ≤ p

Tactic:
simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) h.le

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) - (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩) = 0

Tactic:
sub_eq_zero,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
⊢ Module.IsTorsionFree Rₚ Sₚ

Tactic:
have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
    Submonoid.map_le_of_le_comap _ <| hM.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _))

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ Module.IsTorsionFree Rₚ Sₚ
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.map (algebraMap R S) M ≤ N

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ ↑M
⊢ (algebraMap R S) x ∈ N
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
obtain ⟨m, hm⟩ := h' y

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
⊢ IsUnit ((algebraMap R S) ↑y)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Injective ⇑f

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Function.Injective ⇑f
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Surjective ⇑f

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Function.Surjective ⇑f
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
rw [← coeSubmodule_span]
    rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩
    refine ⟨y, hy, z, ?_⟩
    rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
⊢ P f

Tactic:
algebraize [f]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ P f
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * x - k * y = 0

Tactic:
sub_eq_zero,

Goal state after:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * x = k * y
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ x * k - y * k = 0

Tactic:
sub_eq_zero,

Goal state after:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ x * k = y * k
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : 1 - y * x = 0
⊢ y * x = 1

Tactic:
sub_eq_zero,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : 1 = y * x
⊢ y * x = 1
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : 1 - y * x = 0
⊢ y * x = 1

Tactic:
sub_eq_zero,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : 1 = y * x
⊢ y * x = 1
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ f.EssFiniteType

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.EssFiniteType
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
have H := coeff_eq_zero_of_natDegree_lt h
    rw [coeff_det_X_add_C_card] at H
    simp at H

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih : M (∑ n ∈ s, C (p.coeff n) * T n)
⊢ M (C (p.coeff n) * T n + ∑ x ∈ s, C (p.coeff x) * T x)

Tactic:
exact h_add A ih

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (algebraMap R[X] R[T;T⁻¹]) p = toLaurent p

Tactic:
algebraMap_eq_toLaurent

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ toLaurent p = toLaurent p
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute (single t.i t.j t.c) M

Tactic:
convert! (h _ _ t.hij).smul_left t.c using 1

Goal state after:
case e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ single t.i t.j t.c = t.c • single t.i t.j 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (M * ((listTransvecRow M).take k).prod) (inr unit) (inl i) =
          if k ≤ i then M (inr unit) (inl i) else 0 by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using! H r le_rfl
  intro k hk
  induction k with
  | zero => simp
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    have A :
      (listTransvecRow M)[n]? =
        ↑(transvection (inr unit) (inl n')
        (-M (inr unit) (inl n') / M (inr unit) (inr unit))) := by
      simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using! hi
        · simpa only [hni.symm, not_le, or_false] using! Nat.lt_succ_iff_lt_or_eq.1 hi

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

Tactic:
@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R), (matPolyEquiv (single i j ((monomial n_1) a))).coeff k = single i j (((monomial n_1) a).coeff k)

Tactic:
intro k x

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ (matPolyEquiv (single i j ((monomial k) x))).coeff k✝ = single i j (((monomial k) x).coeff k✝)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommSemiring S
f : S →+* Matrix n n R
⊢ (evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (evalRingHom 0)

Tactic:
ext <;> simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

Goal state after: