mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj P).map f ≫
        match Y with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
      (match X with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
        I.multicospan.map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _) <;>
          simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id]

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst a✝)

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd a✝)

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ f = g

Tactic:
apply hK.hom_ext
  rintro (_ | b)
  · apply h
  · dsimp
    rw [app_right_eq_ι_comp_fst, reassoc_of% h]

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

Goal state before:
pp: case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
⊢ I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)) = I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y))

Tactic:
have := c.condition ⟨⟨y, x⟩, hxy⟩

Goal state after:
case inr.inr
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x y : ι
hxy : y < x
this :
  I.toLinearOrder.fst ⟨(y, x), hxy⟩ ≫ c.π ((MultispanShape.ofLinearOrder ι).fst ⟨(y, x), hxy⟩) =
    I.toLinearOrder.snd ⟨(y, x), hxy⟩ ≫ c.π ((MultispanShape.ofLinearOrder ι).snd ⟨(y, x), hxy⟩)
⊢ I.fst (x, y) ≫ c.π ((MultispanShape.prod ι).fst (x, y)) = I.snd (x, y) ≫ c.π ((MultispanShape.prod ι).snd (x, y))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : PreservesLimitsOfShape J R
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) :=
  comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape._proof_1 R
⊢ PreservesLimitsOfShape J (comonadicRightAdjoint R ⋙ R)

Tactic:
apply CategoryTheory.Limits.comp_preservesLimitsOfShape _ _

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
S.mkQ_surjective.forall,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M), S.mkQ x ≠ 0 → r • S.mkQ x = 0 → ∃ n, r ^ n • ⊤ = ⊥
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
this✝ : Module (Localization p) N := IsLocalizedModule.module p f
this : IsScalarTower R (Localization p) N
⊢ localized₀ p f (⨆ i, g i) = ⨆ i, localized₀ p f (g i)

Tactic:
simpa using! congr_arg (restrictScalars R) (localized'_iSup (Localization p) p f g)

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

Goal state before:
pp: 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
J : Ideal S
x : S
hJ : x ∈ J
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.under R J)

Tactic:
by
    obtain ⟨r, s, hx⟩ := exists_mk'_eq M x
    rw [← hx] at hJ ⊢
    exact
      Ideal.mul_mem_right _ _
        (Ideal.mem_map_of_mem _
          (show (algebraMap R S) r ∈ J from
            mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

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

Goal state before:
pp: 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
⊢ IsLocalization (Submonoid.comap (algebraMap R S) N) T

Tactic:
convert! localization_localization_isLocalization M N T using 1

Goal state after:
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.comap (algebraMap R S) N = localizationLocalizationSubmodule M 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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : ↥M
⊢ (algebraMap R T) x = (algebraMap S T) (mk' S x y) * (algebraMap R T) ↑⟨↑y, ⋯⟩

Tactic:
by simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec]

Goal state after:
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 : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ mk' S 1 z • (algebraMap R S) y = mk' S y z

Tactic:
smul_eq_mul,

Goal state after:
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 : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ mk' S 1 z * (algebraMap R S) y = mk' S y z
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mpr
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 : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ mk' S y z = mk' S 1 z • (algebraMap R S) y

Tactic:
smul_eq_mul,

Goal state after:
case mpr
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 : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ mk' S y z = mk' S 1 z * (algebraMap R S) y
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝

Tactic:
intro h s hs hs'
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
    exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

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

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s hs hs'
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
    exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := ⋯
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (IsLocalization.Away.map R T f 1).comp (algebraMap R R)

pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := ⋯
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ (IsLocalization.Away.map R T f 1).comp (algebraMap R R) = IsLocalization.Away.map R T f 1

Tactic:
· rw [IsLocalization.Away.map, IsLocalization.map_comp]; rfl

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := ⋯
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ (IsLocalization.Away.map R T f 1).comp (algebraMap R R) = IsLocalization.Away.map R T f 1
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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝³ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝² : IsLocalization.Away 1 R
this✝¹ : IsLocalization.Away (f 1) T
this✝ : RingHomInvPair ↑e ↑e.symm
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
| f.comp e.toRingHom

Tactic:
← this,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝³ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝² : IsLocalization.Away 1 R
this✝¹ : IsLocalization.Away (f 1) T
this✝ : RingHomInvPair ↑e ↑e.symm
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
| ((IsLocalization.Away.map R T f 1).comp e.symm.toRingHom).comp e.toRingHom
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : ∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) ⊥

Tactic:
simpa using h P hP

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ Aᵀ.map f = A.map f

Tactic:
h.eq

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ A.map f = A.map f
Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : 0 = 1
⊢ False

Tactic:
exact zero_ne_one this

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

Goal state before:
pp: case inl
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Subsingleton R
⊢ Module.rank S N = Module.rank R N

pp: case inr
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Module.rank S N = Module.rank R N

Tactic:
· have := (algebraMap R S).codomain_trivial; simp only [rank_subsingleton]

Goal state after:
case inr
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Module.rank S N = Module.rank R N
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
  haveI h : pSₚ = Ideal.map (algebraMap S Sₚ) pS := by
    rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
  refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
  · rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
      Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq, ← under_def, under_map_eq_map]
  · intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
      (Algebra.algebraMapSubmonoid S p.primeCompl) x
    obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
    obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ := by
      obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
      refine ⟨β, α * β - 1, ?_, ?_⟩
      · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
          map_mul, hβ, mul_inv_cancel₀, sub_self]
        rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
      · rw [add_sub_cancel]
    use β • x
    rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
      RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
    rw [h, IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
    refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
    · rw [Algebra.smul_def]
      apply Ideal.mul_mem_right
      exact Ideal.mem_map_of_mem _ hγ
    simp only
    rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
      IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]

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

Goal state before:
pp: case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
i : n
⊢ A.cramerMap (c✝ • x✝) i = (c✝ • A.cramerMap x✝) i

Tactic:
· apply (cramerMap_is_linear A i).2

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f.coeff n = 0

Tactic:
degree,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.coeff.support.max = ⊥
n : ℤ
⊢ f.coeff n = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (C a * T n).degree = ↑n

Tactic:
degree,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (C a * T n).coeff.support.max = ↑n
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
inst✝¹ : Semiring R✝
R : Type u_3
inst✝ : Semiring R
x y : R[X]
z : R[T;T⁻¹]
⊢ (x • y) • z = x • y • z

Tactic:
smul_eq_mul,

Goal state after:
R✝ : Type u_1
S : Type u_2
inst✝¹ : Semiring R✝
R : Type u_3
inst✝ : Semiring R
x y : R[X]
z : R[T;T⁻¹]
⊢ (x * y) • z = x • y • z
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j k : n
⊢ Aᵀ.cramer (Pi.single k (A i k • 1)) j = Aᵀ.cramer (Pi.single k (A i k)) j

Tactic:
smul_eq_mul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j k : n
⊢ Aᵀ.cramer (Pi.single k (A i k * 1)) j = Aᵀ.cramer (Pi.single k (A i k)) j
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1, A i j_1 * A.adjugate j_1 j = A.det • if i = j then 1 else 0

Tactic:
smul_eq_mul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1, A i j_1 * A.adjugate j_1 j = A.det * if i = j then 1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 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 = single t.i t.j (t.c • 1)

Tactic:
smul_eq_mul,

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 = single t.i t.j (t.c * 1)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
let n' : Fin r := ⟨n, hn⟩

Goal state after:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ ↑i then 0 else M (inl i) (inr ())
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: p : Type u_4
R : Type u_6
inst✝³ : Fintype p
inst✝² : AddCommMonoid R
inst✝¹ : DecidableEq p
m : p → Type u_8
inst✝ : (i : p) → Fintype (m i)
M : (i : p) → Matrix (m i) (m i) R
⊢ (blockDiagonal' M).trace = ∑ i, (M i).trace

Tactic:
simp [blockDiagonal', trace, Finset.sum_sigma']

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ = 0

Tactic:
by
  rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]

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

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ Function.Surjective A.mulVec ↔ IsUnit A

Tactic:
mulVec_surjective_iff_exists_right_inverse,

Goal state after:
m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (∃ B, A * B = 1) ↔ IsUnit A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ (↑h.unit⁻¹ * A.det) • 1 = 1

Tactic:
h.val_inv_mul,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ 1 • 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v

Tactic:
rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]

Goal state after:
n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ matPolyEquiv.symm (C M) = M.map ⇑C

Tactic:
simp [matPolyEquiv]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ eval r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
Polynomial.eval,

Goal state after:
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ eval₂ (RingHom.id R) r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det