mathlib-initiative/mathlib-tactics huggingface dataset:
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 : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
⊢ OfLocalizationSpan P

Tactic:
introv R hs hs'

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
⊢ P f
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 : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
⊢ ((Localization.awayMap f ↑r).comp (algebraMap R (Localization.Away ↑r))) x =
    (((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away ↑r))) x

Tactic:
have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
      rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
this : fᵣ ((algebraMap R Rᵣ) x) = (algebraMap S Sᵣ) (f x)
⊢ ((Localization.awayMap f ↑r).comp (algebraMap R (Localization.Away ↑r))) x =
    (((e₂.toRingHom.comp fᵣ).comp e₁.toRingHom).comp (algebraMap R (Localization.Away ↑r))) x
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: 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)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
⊢ p = ∑ n ∈ p.coeff.support, C (p.coeff n) * T n

Tactic:
ext a

Goal state after:
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)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ n ∈ p.coeff.support, C (p.coeff n) * T n).coeff a
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
⊢ (comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r) = toFinsupp 0

Tactic:
ext a

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
a : ℕ
⊢ ((comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r)).coeff a = (toFinsupp 0).coeff a
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 α
b : n → α
⊢ A *ᵥ A.cramer b = A.det • b

Tactic:
by
  rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]

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

Goal state before:
pp: case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
h_card,

Goal state after:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ A.adjugate.det = A.det ^ (0 - 1)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A * ⅟C = B
⊢ A = B * C

pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A = B * C
⊢ A * ⅟C = B

Tactic:
· rw [← h, Matrix.invOf_mul_cancel_right]

Goal state after:
case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A = B * C
⊢ A * ⅟C = B
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det

Tactic:
← kroneckerMapBilinear_mul_mul f h_comm,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) (A * 1)) (1 * B)).det
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ (blockDiagonal d).BlockTriangular Prod.snd

Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
  rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']
  exact h

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

Goal state before:
pp: m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.IsUpperTriangular
this : DecidableEq R
⊢ ∏ x, (M.toSquareBlock id x).det = ∏ i, M i i

Tactic:
det_toSquareBlock_id

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f)

Tactic:
ext i j
  by_cases h : i = j <;> simp [h, charmatrix, diagonal]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
⊢ (scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) =
    fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)

Tactic:
ext (i | i) (j | j) : 2

Goal state after:
case inl.inl
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i j : m
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inl i) (Sum.inl j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inl i) (Sum.inl j)).coeff
      n✝

case inl.inr
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i : m
j : n
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inl i) (Sum.inr j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inl i) (Sum.inr j)).coeff
      n✝

case inr.inl
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i : n
j : m
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inr i) (Sum.inl j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inr i) (Sum.inl j)).coeff
      n✝

case inr.inr
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i j : n
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inr i) (Sum.inr j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inr i) (Sum.inr j)).coeff
      n✝
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsEmpty n
A : Matrix n n R
⊢ A.charpoly = 1

Tactic:
by
  simp [charpoly]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ charpoly 0 = X ^ Fintype.card n

Tactic:
by
  simp [charpoly]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
d : n → R
⊢ (diagonal d).charpoly = ∏ i, (X - C (d i))

Tactic:
by
  simp [charpoly]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ charpoly 1 = (X - 1) ^ Fintype.card n

Tactic:
by
  simp [charpoly]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
k : ℕ
⊢ (↑k).charpoly = (X - ↑k) ^ Fintype.card n

Tactic:
by
  simp [charpoly]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ Mᵀ.charpoly = M.charpoly

Tactic:
by
  simp [charpoly]

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
⊢ (diagonal D).det = M.det

Tactic:
by simp [h]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this : fromBlocks A 0 C D * ⅟(fromBlocks A 0 C D) = 1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1

Tactic:
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂) =
    1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1
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
i✝ j✝ : n
⊢ a₁✝ * a₂✝ * ∑ j, (algebraMap R A) (b₁✝ i✝ j) * (algebraMap R A) (b₂✝ j j✝) =
    ∑ x, a₁✝ * (algebraMap R A) (b₁✝ i✝ x) * (a₂✝ * (algebraMap R A) (b₂✝ x j✝))

Tactic:
Finset.mul_sum,

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
⊢ ∑ i, a₁✝ * a₂✝ * ((algebraMap R A) (b₁✝ i✝ i) * (algebraMap R A) (b₂✝ i j✝)) =
    ∑ x, a₁✝ * (algebraMap R A) (b₁✝ i✝ x) * (a₂✝ * (algebraMap R A) (b₂✝ x j✝))
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this : ⅟(fromBlocks A 0 C D) * fromBlocks A 0 C D = 1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1

Tactic:
rw [← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)), fromBlocks_multiply] at this

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * C)
      ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * D)
      ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * C)
      ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D) =
    1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
ha : IsNilpotent a
t : R
⊢ IsNilpotent (t • a)

Tactic:
obtain ⟨k, ha⟩ := ha

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
t : R
k : ℕ
ha : a ^ k = 0
⊢ IsNilpotent (t • a)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : ¬HasFiniteSupport f
⊢ IsNilpotent (finsum f)

Tactic:
· simp only [finsum_def, dif_neg h, IsNilpotent.zero]

Goal state after:
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 ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), f x ∈ I • ⊤

Tactic:
exact fun x => hI (LinearMap.mem_range_self f x)

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h✝ : p.FG
h : p = ⊥
⊢ p.spanFinrank = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∑ x,
      ((eval 0 (derivative ((-1) ^ ↑x)) * eval 0 (1 0 x) + (-1) ^ ↑x * (eval 0 (derivative (1 0 x)) + M 0 x)) *
          eval 0 (submatrix 1 Fin.succ x.succAbove).det +
        (-1) ^ ↑x * eval 0 (1 0 x) *
          eval 0 (derivative (submatrix 1 Fin.succ x.succAbove + X • (M.submatrix Fin.succ x.succAbove).map ⇑C).det)) =
    M.trace

Tactic:
rw [Finset.sum_eq_single 0]

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
        eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
      (-1) ^ ↑0 * eval 0 (1 0 0) *
        eval 0
          (derivative
            (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
    M.trace

case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∀ b ∈ univ,
    b ≠ 0 →
      (eval 0 (derivative ((-1) ^ ↑b)) * eval 0 (1 0 b) + (-1) ^ ↑b * (eval 0 (derivative (1 0 b)) + M 0 b)) *
            eval 0 (submatrix 1 Fin.succ b.succAbove).det +
          (-1) ^ ↑b * eval 0 (1 0 b) *
            eval 0 (derivative (submatrix 1 Fin.succ b.succAbove + X • (M.submatrix Fin.succ b.succAbove).map ⇑C).det) =
        0

case succ.h₁
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ 0 ∉ univ →
    (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
          eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
        (-1) ^ ↑0 * eval 0 (1 0 0) *
          eval 0
            (derivative
              (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
      0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
⊢ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Tactic:
n

Goal state after:
case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
⊢ p.coeff n ∈ Set.range ⇑f
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
⊢ ∃ q, map f q = p ∧ q.support = p.support

Tactic:
let q : R[X] := ∑ k ∈ p.support, monomial k (g k)

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
⊢ ∃ q, map f q = p ∧ q.support = p.support
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑((a + b).choose a) = ↑(a + b)! / (↑a ! * ↑b !)

Tactic:
by
  rw [cast_choose K (le_add_right _ _), Nat.add_sub_cancel_left]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
⊢ (∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k).degree < ↑p.natDegree

Tactic:
← Fin.sum_univ_eq_sum_range,

Goal state after:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
⊢ (∑ i, C (g ↑i) * X ^ ↑i).degree < ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
hasseDeriv_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (f.sum fun i r ↦ (monomial (i - k)) (↑(i.choose k) * r)).coeff n = ↑((n + k).choose k) * f.coeff (n + k)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (hasseDeriv n) p = 0

Tactic:
hasseDeriv_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (p.sum fun i r ↦ (monomial (i - n)) (↑(i.choose n) * r)) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree ≤ p.natDegree - n

Tactic:
hasseDeriv_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun i r ↦ (monomial (i - n)) (↑(i.choose n) * r)).natDegree ≤ p.natDegree - n