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

Goal state before:
pp: case surj
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
· intro s
      obtain ⟨t, ht, ht', h⟩ := hσ s
      exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩

Goal state after:
case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ {x y : ↥(adjoin R ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y
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
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
h : IsLocalRing S
⊢ mk' S x y ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using!
      isUnit_mk'_iff S I x y

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

Goal state before:
pp: 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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s) * (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x) *
      (equivQuotMaximalIdeal p Rₚ) (((Ideal.Quotient.mk p) ↑s)⁻¹ * (Ideal.Quotient.mk p) ↑s)

Tactic:
inv_mul_cancel₀ h₁,

Goal state after:
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ₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s) * (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) x) * (equivQuotMaximalIdeal p Rₚ) 1
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
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 : ℕ
⊢ ∀ a ∈ p ^ n, (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) a = 0

Tactic:
simp_rw [ofId_apply, ← RingHom.mem_ker, ← SetLike.le_def]
    rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]

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 := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
have : IsLocalization.Away (1 : R) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one (Equiv.refl _).bijective

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 := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp 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 : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hT : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)
⊢ P f

Tactic:
apply hP _ s hs
  intro r
  obtain ⟨T, _, _, _, hT⟩ := hT r
  convert! hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT
  rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]

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

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
by
  introv R hs hf
  exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

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

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
by
  introv R hs hf
  exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩

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

Goal state before:
pp: case mul_T.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)))

Tactic:
convert QT _ _

Goal state after:
case mul_T.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)) * T 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
⊢ (fun i_1 ↦ A.updateRow i (Pi.single j 1) (σ i_1) i_1) = fun i_1 ↦ A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
ext j'

Goal state after:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
j' : n
⊢ A.updateRow i (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single i 1) (σ j') j'
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j ↦ Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ ((A.submatrix ⇑e ⇑e).updateRow j (Pi.single i 1)).det = A.adjugate.submatrix (⇑e) (⇑e) i j

Tactic:
submatrix_apply,

Goal state after:
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j ↦ Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ ((A.submatrix ⇑e ⇑e).updateRow j (Pi.single i 1)).det = A.adjugate (e i) (e j)
Module: Mathlib.Algebra.Polynomial.Laurent

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

Tactic:
← mul_one (C a),

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * 1).degree = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b <;>
    simp [ha, hb, hab, e.eq_symm_apply, single]

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

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

Tactic:
by rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]

Goal state after:
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
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype m'
inst✝⁷ : NonUnitalNonAssocSemiring α
inst✝⁶ : NonUnitalNonAssocSemiring β
inst✝⁵ : NonUnitalNonAssocSemiring γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
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 l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ (∑ x, f (A i x * B x j)) (∑ j, A' i' j * B' j j') = ∑ x, ∑ x_1, (f (A i x)) (A' i' x_1) * (f (B x j)) (B' x_1 j')

Tactic:
LinearMap.sum_apply,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype m'
inst✝⁷ : NonUnitalNonAssocSemiring α
inst✝⁶ : NonUnitalNonAssocSemiring β
inst✝⁵ : NonUnitalNonAssocSemiring γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
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 l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ∑ d, (f (A i d * B d j)) (∑ j, A' i' j * B' j j') = ∑ x, ∑ x_1, (f (A i x)) (A' i' x_1) * (f (B x j)) (B' x_1 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 : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, A.submatrix (⇑e.symm) (⇑e.symm) (e i) x * A.adjugate.submatrix (⇑e.symm) (⇑e.symm) x (e i)
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
submatrix_apply,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, A (e.symm (e i)) (e.symm x) * A.adjugate (e.symm x) (e.symm (e i))
⊢ A.det = ∑ j, A i j * A.adjugate j i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
· 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: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((⅟(diagonal v).det • fun i ↦ ∏ j ∈ univ.erase i, v j) * v) i = 1 i

Tactic:
dsimp

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (⅟(diagonal v).det * ∏ j ∈ univ.erase i, v j) * v i = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (v * ⅟(diagonal v).det • fun i ↦ ∏ j ∈ univ.erase i, v j) i = 1 i

Tactic:
dsimp

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ v i * (⅟(diagonal v).det * ∏ j ∈ univ.erase i, v j) = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: R : Type u_9
inst✝ : Semiring R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
x✝ j : Fin n
h : id j < id x✝
⊢ of (fun i j ↦ (p j).coeff ↑i) x✝ j = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
by
  suffices ∀ cn, Fintype.card n = cn →
      ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D by exact this _ rfl
  intro cn hn
  induction cn generalizing n M with
  | zero =>
    refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
    ext i j
    rw [Fintype.card_eq_zero_iff] at hn
    exact hn.elim' i
  | succ r IH =>
    have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp
    apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
    apply
      exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
        IH (Fin r) N (by simp)

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 α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) (⅟A * B + -(⅟A * B * ⅟D) * D) 0 (⅟D * D) = 1

Tactic:
Matrix.neg_mul,

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 α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) (⅟A * B + -(⅟A * B * ⅟D * D)) 0 (⅟D * D) = 1
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 A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) 0 (-(⅟D * C * ⅟A) * A + ⅟D * C) (⅟D * D) = 1

Tactic:
Matrix.neg_mul,

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 A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) 0 (-(⅟D * C * ⅟A * A) + ⅟D * C) (⅟D * D) = 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₂✝) • (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✝

Tactic:
dsimp

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.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
have hD := hAD.mp hA
    cases hA.nonempty_invertible
    cases hD.nonempty_invertible
    let := fromBlocksZero₂₁Invertible A B D
    simp_rw [← invOf_eq_nonsing_inv, invOf_fromBlocks_zero₂₁_eq]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + A * B).det = (1 - -A * B).det

Tactic:
Matrix.neg_mul,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + A * B).det = (1 - -(A * B)).det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case h
R : Type u_1
x : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0

Tactic:
rw [neg_pow, hn, mul_zero]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ ∑ x_1 ∈ f.support, ((RingHom.id R) (f.coeff x_1) * x ^ x_1 - (RingHom.id R) (f.coeff x_1) * y ^ x_1) =
    ∑ i ∈ f.support, f.coeff i * ↑(powSubPowFactor x y i) * (x - y)

Tactic:
dsimp

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ ∑ x_1 ∈ f.support, (f.coeff x_1 * x ^ x_1 - f.coeff x_1 * y ^ x_1) =
    ∑ i ∈ f.support, f.coeff i * ↑(powSubPowFactor x y i) * (x - y)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsNilpotent x
⊢ ¬¬IsNilpotent x

Tactic:
by simpa only [not_not] using hx

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ (∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a

Tactic:
· exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h),

Goal state after:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (∏ i, (X - C (M i i))).natDegree = Fintype.card n
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : Set M
hs : Cardinal.mk ↑s = (restrictScalars R (span S s)).spanRank
e : span R s = restrictScalars R (span S s)
⊢ (span S s).spanRank ≤ (restrictScalars R (span S s)).spanRank

Tactic:
grw [← hs, spanRank_span_le_card]

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

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ submatrix 1 Fin.succ i.succAbove j 0 = 0

Tactic:
submatrix_apply,

Goal state after:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ 1 j.succ (i.succAbove 0) = 0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case neg
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 : ℕ
hn : ¬p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

Tactic:
exact h <| coeff_mem_coeffs hn

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

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) X - (expand K k) (C ((M ^ k) j j))).coeff m =
    ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j

Tactic:
expand_C,

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) X - C ((M ^ k) j j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j