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

Goal state before:
pp: R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this✝¹ : Algebra (Localization (Submonoid.map f M)) S' := ⋯
this✝ : IsScalarTower S (Localization (Submonoid.map f M)) S'
this : IsLocalization (Submonoid.map (algebraMap S (Localization (Submonoid.map f M))) T) S'
⊢ (IsLocalization.map S' f hy).comp (algebraMap R R') =
    ((algebraMap (Localization (Submonoid.map f M)) S').comp
          (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯)).comp
      (algebraMap R R')

Tactic:
ext

Goal state after:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this✝¹ : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this✝ : IsScalarTower S (Localization (Submonoid.map f M)) S'
this : IsLocalization (Submonoid.map (algebraMap S (Localization (Submonoid.map f M))) T) S'
x✝ : R
⊢ ((IsLocalization.map S' f hy).comp (algebraMap R R')) x✝ =
    (((algebraMap (Localization (Submonoid.map f M)) S').comp
            (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯)).comp
        (algebraMap R R'))
      x✝
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, g₁ x = g₂ x
⊢ g₁ = g₂

Tactic:
algebraize [f, g₁.comp f]
  ext x
  exact DFunLike.congr_fun (Algebra.EssFiniteType.algHom_ext T
    ⟨g₁, fun _ ↦ rfl⟩ ⟨g₂, DFunLike.congr_fun h₁.symm⟩ h₂) x

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
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
constructor

Goal state after:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P

case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P
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ₚ
n : ℕ
⊢ (((Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) ⋯).comp
              (Quotient.liftₐ (maximalIdeal Rₚ ^ n) (liftAlgHom ⋯) ⋯)).comp
          (Quotient.mkₐ R (maximalIdeal Rₚ ^ n))).comp
      (algHom R R Rₚ) =
    ((AlgHom.id R (Rₚ ⧸ maximalIdeal Rₚ ^ n)).comp (Quotient.mkₐ R (maximalIdeal Rₚ ^ n))).comp (algHom R R Rₚ)

Tactic:
ext

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

Goal state before:
pp: case refine_4
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ₚ
n : ℕ
⊢ ((Quotient.liftₐ (maximalIdeal Rₚ ^ n) (liftAlgHom ⋯) ⋯).comp
          (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) ⋯)).comp
      (Quotient.mkₐ R (p ^ n)) =
    (AlgHom.id R (R ⧸ p ^ n)).comp (Quotient.mkₐ R (p ^ n))

Tactic:
ext

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[T;T⁻¹]
h : ∀ (a : ℤ), p.coeff a = q.coeff a
⊢ p = q

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[T;T⁻¹]
h : ∀ (a : ℤ), p.coeff a = q.coeff a
a✝ : ℤ
⊢ p.coeff a✝ = q.coeff a✝
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inl
R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
simp only [rank_subsingleton, lift_one]

Goal state after:
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 α
⊢ IsLinearMap α A.cramerMap

Tactic:
constructor

Goal state after:
case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y

case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) ↔
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x

Tactic:
constructor

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x

case mpr
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
⊢ adjugate 1 = 1

Tactic:
ext

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i✝ j✝ : n
⊢ adjugate 1 i✝ j✝ = 1 i✝ j✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℤ
hn : 0 ≤ n
⊢ (eval₂ f x) (T n) = ↑(x ^ n)

pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℤ
hn : n < 0
⊢ (eval₂ f x) (T n) = ↑(x ^ n)

Tactic:
· lift n to ℕ using hn
    apply eval₂_T_n

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℤ
hn : n < 0
⊢ (eval₂ f x) (T n) = ↑(x ^ n)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Subsingleton R
this : Subsingleton T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
simp only [rank_subsingleton, lift_one]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ ⇑invert ∘ ⇑C = ⇑C

Tactic:
ext

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝).coeff a✝ = (C x✝).coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
t : R
⊢ invert (C t) = C t

Tactic:
ext

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)).coeff a✝ = (C t).coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
⊢ invert (invert x✝) = x✝

Tactic:
ext

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)).coeff a✝ = x✝.coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
⊢ (f + g).smeval x = f.smeval x + g.smeval x

Tactic:
by
  simp [smeval, Finsupp.sum_add_index, add_smul]

Goal state after:
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 α
hA : IsLeftRegular A.det
⊢ IsRegular A

Tactic:
constructor

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsLeftRegular A

case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRightRegular A
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
⊢ A <• ↑b = b •> A

Tactic:
ext

Goal state after:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
A : Matrix l m α
b : ℕ
x✝ : n
i✝ : l
j✝ : m
⊢ (A <• ↑b) i✝ j✝ = (b •> A) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ (fun i ↦ ↑a •> B) = fun x ↦ a •> B

Tactic:
ext

Goal state after:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
x✝ : l
i✝ : m
j✝ : n
⊢ (↑a •> B) i✝ j✝ = (a •> B) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ

Tactic:
ext

Goal state after:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ = (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap

Tactic:
ext

Goal state after:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ =
    (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
⊢ (kroneckerMap (tmul R) x y)ᴴ = kroneckerMap (tmul R) xᴴ yᴴ

Tactic:
ext

Goal state after:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (tmul R) x y)ᴴ i✝ j✝ = kroneckerMap (tmul R) xᴴ yᴴ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
M✝ : Matrix n n α
⊢ f' (g M✝) = M✝

Tactic:
ext

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
M✝ : Matrix n n α
i✝ j✝ : n
⊢ f' (g M✝) i✝ j✝ = M✝ i✝ j✝
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 α
inst✝ : Invertible A.det
⊢ A.unitOfDetInvertible = A.nonsingInvUnit ⋯

Tactic:
ext

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A.det
i✝ j✝ : n
⊢ ↑A.unitOfDetInvertible i✝ j✝ = ↑(A.nonsingInvUnit ⋯) i✝ j✝
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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
constructor

Goal state after:
case left
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0

case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0

Tactic:
· ext i j
    have : i = unit := by simp only
    simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
⊢ (fun i ↦ k ≤ b i) = q

Tactic:
ext

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := ⋯
q : m → Prop := ⋯
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this : Invertible (M.toBlock p p)
x✝ : m
⊢ k ≤ b x✝ ↔ q x✝
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : (matPolyEquiv (single i j p)).coeff k = single i j (p.coeff k)
hq : (matPolyEquiv (single i j q)).coeff k = single i j (q.coeff k)
⊢ (matPolyEquiv (single i j (p + q))).coeff k = single i j ((p + q).coeff k)

Tactic:
ext

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k

Tactic:
constructor

Goal state after:
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

Goal state after:
case h₁
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
x✝ : S
i✝ j✝ : n
⊢ (((evalRingHom 0).mapMatrix.comp f.polyToMatrix).comp C) x✝ i✝ j✝ = ((f.comp (evalRingHom 0)).comp C) x✝ i✝ j✝

case h₂
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
i✝ j✝ : n
⊢ ((evalRingHom 0).mapMatrix.comp f.polyToMatrix) X i✝ j✝ = (f.comp (evalRingHom 0)) X i✝ j✝
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 : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ (evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X]) =
    (compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x✝ : Matrix m m (Matrix n n R[X])
i✝ j✝ : m × n
⊢ ((evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X])) x✝ i✝ j✝ =
    ((compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix) x✝ i✝ j✝
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (a₁✝ * a₂✝) • (b₁✝.map ⇑(algebraMap R A) * b₂✝.map ⇑(algebraMap R A)) =
    a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ j✝ : n
⊢ ((a₁✝ * a₂✝) • (b₁✝.map ⇑(algebraMap R A) * b₂✝.map ⇑(algebraMap R A))) i✝ j✝ =
    (a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)) i✝ j✝
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
⊢ IsUnit P

pp: case neg
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
⊢ IsUnit P

Tactic:
· rw [eq_C_of_natDegree_eq_zero hdeg]
    exact hunit.map C

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
⊢ IsUnit P
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), ∑ i, A i j • b i = f (b j)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i, A i j • b i = f (b j)

case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i, A i j • b i = f (b j)) → Represents b A f