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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ ((p₁ * p₂).sum fun a b ↦ if a = k then a₁ * a₂ * (algebraMap R A) b else 0) =
    ((p₁.sum fun n r ↦ (monomial n) (a₁ * (algebraMap R A) r)) *
          p₂.sum fun n r ↦ (monomial n) (a₂ * (algebraMap R A) r)).coeff
      k

Tactic:
sum_def,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (∑ n ∈ (p₁ * p₂).support, if n = k then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff n) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ a ⊗ₜ[R] (a_1 • X ^ n)) = a ⊗ₜ[R] p

Tactic:
sum_def,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ ∑ n ∈ p.support, a ⊗ₜ[R] (p.coeff n • X ^ n) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R
e : g (mk' S (x - y) 1) = 0
r : R
hr : r ∈ M
hr' : r * (x - y) ∈ RingHom.ker f
⊢ ↑⟨f r, ⋯⟩ * f x = ↑⟨f r, ⋯⟩ * f y

Tactic:
simpa [sub_eq_zero, mul_sub] using hr'

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

Goal state before:
pp: case refine_1
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
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ y z, (algebraMap R S) (↑c * z') = ↑y * (algebraMap R S) ↑z

Tactic:
refine ⟨z, c * s, ?_⟩

Goal state after:
case refine_1
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
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ (algebraMap R S) (↑c * z') = ↑z * (algebraMap R S) ↑(c * s)
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
x : Ideal R
H : x.IsPrime
inst✝ : IsDomain R
⊢ x.primeCompl ≤ nonZeroDivisors R

Tactic:
by
      intro a ha
      rw [mem_nonZeroDivisors_iff_ne_zero]
      exact fun h => ha (h.symm ▸ x.zero_mem)

Goal state after:
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₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
h₁ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) ↔
    (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁)
this :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) →
    ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂

Tactic:
h₂,

Goal state after:
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₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
h₁ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) ↔
    (algebraMap S T) x₁ = (algebraMap S T) x₂
h₂ :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) * (algebraMap S T) ((algebraMap R S) ↑s₂) ↔
    (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁)
this :
  (algebraMap S T) x₁ * (algebraMap S T) ((algebraMap R S) ↑s₁) =
      (algebraMap S T) x₂ * (algebraMap S T) ((algebraMap R S) ↑s₁) →
    ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
⊢ (algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr
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 ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
· constructor; constructor
    · exact fun y ↦ y.prop
    · intro s
      obtain ⟨t, ht, ht', h⟩ := hσ s
      exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩
    · intro x y e
      exact ⟨1, by simpa using Subtype.ext e⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R (under S (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p

Tactic:
under_map_of_isPrime_disjoint _ _ ‹_› disj,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R P) = Ideal.map (algebraMap R R') p
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
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : LinearIndepOn R id ↑s
inst✝ : DecidableEq S
⊢ LinearIndepOn R id ↑(commonDenomOfFinset M s • s)

Tactic:
linearIndepOn_finset_iff

Goal state after:
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
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : ∀ (f : A → R), ∑ i ∈ s, f i • id i = 0 → ∀ i ∈ s, f i = 0
inst✝ : DecidableEq S
⊢ ∀ (f : A → R), ∑ i ∈ commonDenomOfFinset M s • s, f i • id i = 0 → ∀ i ∈ commonDenomOfFinset M s • s, f i = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (f * T ↑n * T (-↑n))

Tactic:
← hf

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (toLaurent f' * T (-↑n))
Module: Mathlib.Algebra.Polynomial.Laurent

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

Tactic:
rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]

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 m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * 1 = A

Tactic:
Matrix.mul_one

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A = A
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
𝕜 : 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⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

pp: case neg
𝕜 : 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⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
· have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [h]
      simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]
      simp [field]

Goal state after:
case neg
𝕜 : 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⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (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: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : Nonempty n
r : R
inhabited_h : Inhabited n
⊢ ∃ a, a.trace = r

Tactic:
exact ⟨single default default r, trace_single_eq_same default r⟩

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 * 1 = A

Tactic:
Matrix.mul_one

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal v⁻¹ʳ

Tactic:
rw [nonsing_inv_eq_ringInverse]
  by_cases h : IsUnit v
  · have := isUnit_diagonal.mpr h
    cases this.nonempty_invertible
    cases h.nonempty_invertible
    rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
  · have := isUnit_diagonal.not.mpr h
    rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]

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

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (A.submatrix ⇑e₁ ⇑e₂)
⊢ 0 = 0 ⇑e₂ ⇑e₁

Tactic:
Pi.zero_apply

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
⊢ M⁻¹.BlockTriangular b

Tactic:
suffices ∀ hs : Finset α, univ.image b = hs → BlockTriangular M⁻¹ b by exact this _ rfl
  intro s hs
  induction s using Finset.strongInduction generalizing m with | H s ih =>
  subst hs
  intro i j hij
  have : Inhabited m := ⟨i⟩
  let k := (univ.image b).max' (univ_nonempty.image _)
  let b' := fun i : { a // b a < k } => b ↑i
  let A := M.toBlock (fun i => b i < k) fun j => b j < k
  obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
  · have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
      simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
    simp [this.symm]
  have : Invertible A := hM.invertibleToBlock _
  have hA : A.BlockTriangular b' := hM.submatrix
  have hb' : image b' univ ⊂ image b univ := by
    convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
    convert! max'_mem (α := α) _ _
  have hij' : b' ⟨j, hij.trans hi⟩ < b' ⟨i, hi⟩ := by simp_rw [b', hij]
  simp [A, hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]

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
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M = M * 1

Tactic:
Matrix.mul_one

Goal state after:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M = M
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✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x y : Matrix m m A ⊗[R] Matrix n n B),
    (kroneckerTMulAlgEquiv m n R S A B) (star x) = star ((kroneckerTMulAlgEquiv m n R S A B) x) →
      (kroneckerTMulAlgEquiv m n R S A B) (star y) = star ((kroneckerTMulAlgEquiv m n R S A B) y) →
        (kroneckerTMulAlgEquiv m n R S A B) (star (x + y)) = star ((kroneckerTMulAlgEquiv m n R S A B) (x + y))

Tactic:
simp_all

Goal state after:
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✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x y : Matrix m m R ⊗[R] Matrix n n R),
    (kroneckerAlgEquiv m n R) (star x) = star ((kroneckerAlgEquiv m n R) x) →
      (kroneckerAlgEquiv m n R) (star y) = star ((kroneckerAlgEquiv m n R) y) →
        (kroneckerAlgEquiv m n R) (star (x + y)) = star ((kroneckerAlgEquiv m n R) (x + y))

Tactic:
simp_all

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

Tactic:
convert!
    Invertible.copy' _ _
      (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D))
        (-(⅟D * C * ⅟(A - B * ⅟D * C))) (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D))
      (fromBlocks_eq_of_invertible₂₂ _ _ _ _) _

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

case convert_6
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible D

case convert_7
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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D) =
    ⅟(fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: case e_a.e_a
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
⊢ (f.sum fun e a ↦ a * ↑e * x ^ (e - 1) * y) = eval x (derivative f) * y

Tactic:
derivative_eval

Goal state after:
case e_a.e_a
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
⊢ (f.sum fun e a ↦ a * ↑e * x ^ (e - 1) * y) = (f.sum fun n a ↦ a * ↑n * x ^ (n - 1)) * y
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n ≤ m + n - 1 + 1

Tactic:
← Nat.sub_le_iff_le_add

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n - 1 ≤ m + n - 1
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ → ∃ S, S.Finite ∧ span R S = p

pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = p) → ⨅ s, #↑↑s < ℵ₀

Tactic:
· rintro h
    obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
    refine ⟨s.1, ?_, s.2⟩
    simpa [← hs] using h

Goal state after:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = p) → ⨅ s, #↑↑s < ℵ₀
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₂ : span R s = I
hs₁ : s = ∅
⊢ I = ⊥

Tactic:
simp_all

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
x✝ : p.IsPrincipal ∧ p ≠ ⊥
a : M
ha : p = R ∙ a
right✝ : p ≠ ⊥
⊢ a ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
p : Submodule R M
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f p).spanRank
e : span S (⇑f '' s) = map f p
⊢ Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank

Tactic:
obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f (span R s)).spanRank
e : span S (⇑f '' s) = map f (span R s)
⊢ Cardinal.lift.{v, u} (span R s).spanRank ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank