mathlib-initiative/mathlib-tactics huggingface dataset:
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ₚ
⊢ R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ

Tactic:
by
  refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
  · rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker, ← under_def,
      Ideal.Quotient.algebraMap_eq, Ideal.mk_ker, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]
  · intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
    obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹
    simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
      Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]
    use x * s'
    rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
    have : algebraMap R Rₚ s ∉ maximalIdeal Rₚ := by
      rw [← Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]
      exact s.prop
    refine ((inferInstance : (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this
    rw [mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left,
      ← map_mul, ← map_sub, ← Ideal.mem_under, under_maximalIdeal Rₚ p,
      mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_mul, hs,
      mul_inv_cancel₀, mul_one, sub_self]
    rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
    exact s.prop

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
⊢ OfLocalizationSpan P

Tactic:
introv R hs hs'
  apply_fun Ideal.map f at hs
  rw [Ideal.map_span, Ideal.map_top] at hs
  apply hP _ _ hs
  rintro ⟨_, r, hr, rfl⟩
  rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r)
    (T := Submonoid.powers (f r))]
  · apply hP' _ r
    exact hs' ⟨r, hr⟩

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 : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this : IsScalarTower R S Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
    inferInstanceAs <| IsLocalization (M.map f) Sᵣ

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this✝ : IsScalarTower R S Sᵣ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)
Module: Mathlib.LinearAlgebra.Dimension.Localization

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

Tactic:
simp only [rank_subsingleton]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ s ∈ f.coeff.support, ↑s = ⊥
⊢ f.coeff n = 0

Tactic:
Finsupp.mem_support_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), f.coeff s ≠ 0 → ↑s = ⊥
⊢ f.coeff n = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a * 1).degree

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a).degree
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

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

Tactic:
mul_one

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * T ↑n = toLaurent p * 1

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * T ↑n = toLaurent p
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ single t.i t.j t.c = single t.i t.j (t.c * 1)

Tactic:
mul_one

Goal state after:
case e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ single t.i t.j t.c = single t.i t.j t.c
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h]

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

Goal state before:
pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
simp [TransvectionStruct.sumInl, transvection, h]

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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n * 1 = A'.det ^ Fintype.card n

Tactic:
mul_one

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ (-1) ^ (↑j + ↑i) * 1 * (A.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0

Tactic:
mul_one

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Matrix.Trace

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

Tactic:
simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]

Goal state after:
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
i : Fin r
⊢ ((listTransvecCol M).prod * M) (inl i) (inr ()) = 0

Tactic:
suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (((listTransvecCol M).drop k).prod * M) (inl i) (inr unit) =
          if k ≤ i then 0 else M (inl i) (inr unit) by
    simpa [List.drop] using H 0
  intro k hk
  induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    let n' : Fin r := ⟨n, hn⟩
    rw [List.drop_eq_getElem_cons hn']
    have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
    simp only [Matrix.mul_assoc, A, List.prod_cons]
    by_cases h : n' = i
    · 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]
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2

Goal state after:
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
i : Fin r
⊢ ((listTransvecCol M).prod * M) (inl i) (inr ()) = 0

Tactic:
by
  suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (((listTransvecCol M).drop k).prod * M) (inl i) (inr unit) =
          if k ≤ i then 0 else M (inl i) (inr unit) by
    simpa [List.drop] using H 0
  intro k hk
  induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    let n' : Fin r := ⟨n, hn⟩
    rw [List.drop_eq_getElem_cons hn']
    have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
    simp only [Matrix.mul_assoc, A, List.prod_cons]
    by_cases h : n' = i
    · 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]
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2

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 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
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
⊢ ∀ (M N : Matrix n n α), f' (g M * g N) = M * N

Tactic:
intro M

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
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
M : Matrix n n α
⊢ ∀ (N : Matrix n n α), f' (g M * g N) = M * N
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
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
⊢ ∀ (M : Matrix n n α), IsRegular (g M).det

Tactic:
intro M

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
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
M : Matrix n n α
⊢ IsRegular (g M).det
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
⊢ M⁻¹ i j = 0

Tactic:
have : Invertible A := hM.invertibleToBlock _

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
⊢ M⁻¹ i j = 0
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
⊢ charmatrix 0 = (scalar n) X

Tactic:
simp [charmatrix]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_3
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]
⊢ (matPolyEquiv (single i' j' x)).coeff k i j = (single i' j' x i j).coeff k

Tactic:
matPolyEquiv_coeff_apply_aux_2

Goal state after:
case refine_3
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]
⊢ single i' j' (x.coeff k) i j = (single i' j' x i j).coeff k
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
M : Type u_9
N : Type u_10
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : Module R N
inst✝⁸ : IsScalarTower R S M
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
a : Matrix l m M
b : Matrix n p N
⊢ (kroneckerTMulLinearEquiv l m n p R S M N).symm (kroneckerMap (tmul R) a b) = a ⊗ₜ[R] b

Tactic:
by
  simp [LinearEquiv.symm_apply_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 m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ A.det * (D - C * ⅟A * B).det * 1 = A.det * (D - C * ⅟A * B).det

Tactic:
mul_one

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 m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ A.det * (D - C * ⅟A * B).det = A.det * (D - C * ⅟A * B).det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0

Tactic:
← zero_isRadical_iff,

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsRadical 0 ↔ ∀ (x : R), x ^ k = 0 → x = 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x + y)

Tactic:
obtain ⟨n, hn⟩ := hx

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: 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)

pp: 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

Tactic:
· intro h i
    have := LinearMap.congr_fun h (Pi.single i 1)
    rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval a) P)

Tactic:
← add_sub_cancel (aeval b P) (aeval a P)

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval b) P + ((aeval a) P - (aeval b) P))
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
⊢ #univ * 1 = #univ

Tactic:
mul_one

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
⊢ #univ = #univ
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).Monic
⊢ M.charpoly.Monic

Tactic:
Monic

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ M.charpoly.leadingCoeff = 1
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✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i, M.diag i = ∑ i, M i i

Tactic:
diag_apply

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{v, u} (Submodule.spanRank I) ≤ Cardinal.lift.{u, v} (Submodule.spanRank (map (↑f) I))

Tactic:
← Ideal.map_of_equiv f (I := I)

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{v, u} (Submodule.spanRank (map (↑f.symm) (map (↑f) I))) ≤
    Cardinal.lift.{u, v} (Submodule.spanRank (map (↑f) I))
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
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ Fintype.card n * 1 = Fintype.card n

Tactic:
mul_one

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ Fintype.card n = Fintype.card n