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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
I : Ideal R
x : ↥M
a b : ↥(Ideal.map (algebraMap R S) I)
e :
  ((algebraMap R (Module.End R ↥(Ideal.map (algebraMap R S) I))) ↑x) a =
    ((algebraMap R (Module.End R ↥(Ideal.map (algebraMap R S) I))) ↑x) b
⊢ (fun x_1 ↦ (algebraMap R S) ↑x * x_1) ↑a = (fun x_1 ↦ (algebraMap R S) ↑x * x_1) ↑b

Tactic:
by simpa [Algebra.smul_def] using congr(($e).1)

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

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
⊢ ∀ (c : ↥P.primeCompl), IsRegular ↑c

Tactic:
exact fun ⟨_, h⟩ ↦ .of_ne_zero <| by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ (mapOfCompatibleSMul A R A M N).ker = Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Tactic:
by
  refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm
  · rintro - ⟨a, m, n, rfl⟩
    simp [smul_tmul]
  · let S := Submodule.span A {(a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) | (a : A) (m : M) (n : N)}
    let F : M ⊗[A] N →ₗ[A] (M ⊗[R] N) ⧸ S := TensorProduct.lift ({
      toFun m := {
        toFun n := S.mkQ (m ⊗ₜ[R] n)
        map_add' _ _ := by simp [tmul_add]
        map_smul' a n := by
          rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]
          exact Submodule.subset_span ⟨a, m, n, rfl⟩ }
      map_add' _ _ := by ext _; simp [add_tmul]
      map_smul' _ _ := by simp; rfl })
    have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ := by ext; simp [S, F]
    change (mapOfCompatibleSMul A R A M N).ker ≤ S
    rw [← Submodule.ker_mkQ S, ← h]
    exact (mapOfCompatibleSMul A R A M N).ker_le_ker_comp F

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
⊢ (TensorProduct.lift (ofId R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}))
          (Ideal.quotientMapₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) φ ⋯) ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) ψ heψ) =
    AlgHom.id R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})

Tactic:
by ext; simp [ψ, φ]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))
⊢ x ∈ I

Tactic:
refine Ideal.mem_of_localization_maximal fun m hm ↦ ?_

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))
m : Ideal R
hm : m.IsMaximal
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Cᵀ = B

Tactic:
← hBC

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (C a * T n).coeff.support.max = ↑n

Tactic:
support_coeff_C_mul_T_of_ne_zero a0 n

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ {n}.max = ↑n
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ Commute (single i j 1) M) i j

Tactic:
j

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
i j : n
⊢ i ≠ j → (fun i j ↦ Commute (single i j 1) M) i j
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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * (⅟C + V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A = 1

Tactic:
rw [Matrix.mul_invOf_cancel_right]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * V * ⅟A = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
B : Matrix m n α
h : IsUnit A.det
⊢ B * A⁻¹ * A = B

Tactic:
simp [Matrix.mul_assoc, nonsing_inv_mul A h]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i : m
⊢ ∀ ⦃j : m⦄, b j < b i → (M * N) i j = 0

Tactic:
j

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
⊢ b j < b i → (M * N) i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
i : m
hi : b i = k
⊢ ∀ (j : m), ¬b j = k → M i j = 0

Tactic:
j

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
i : m
hi : b i = k
j : m
⊢ ¬b j = k → M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H
α : 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 : m
⊢ ∀ ⦃j : m⦄, b j < b i → M⁻¹ i j = 0

Tactic:
j

Goal state after:
case H
α : 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
⊢ b j < b i → M⁻¹ i j = 0
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 ((⅟(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

Tactic:
replace := congr_arg Matrix.toBlocks₂₂ 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)).toBlocks₂₂ =
    toBlocks₂₂ 1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: 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 0 (-(1 * (⅟D * C) * 1)) 1 *
      (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 ⅟D * fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)

Tactic:
simp only [fromBlocks_multiply, Matrix.one_mul, Matrix.mul_one, Matrix.zero_mul,
      Matrix.mul_zero, add_zero, zero_add, neg_zero, Matrix.mul_neg, Matrix.neg_mul, neg_neg, ←
      Matrix.mul_assoc, add_comm (⅟D)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
⊢ IsNilpotent (C r)

Tactic:
obtain ⟨k, hk⟩ := hpr

Goal state after:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ IsNilpotent (C r)
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (M * N).FG

Tactic:
by
  rw [mul_eq_map₂]; exact hm.map₂ _ hn

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

Goal state before:
pp: case pos
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
⊢ M.charmatrix.det.degree = ↑0

Tactic:
det_eq_one_of_card_eq_zero

Goal state after:
case pos
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
⊢ degree 1 = ↑0

case pos
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
⊢ Fintype.card n = 0
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
⊢ p.generators.ncard = p.spanFinrank

Tactic:
by
  rw [← Nat.cast_inj (R := Cardinal), ← fg_iff_spanRank_eq_spanFinrank.mpr h, Set.ncard, Set.encard,
     ENat.card, generators_card, toNat_toENat, ← spanFinrank]
  exact (fg_iff_spanRank_eq_spanFinrank.mpr h).symm

Goal state after:
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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (M.charpoly - ∏ i, (X - C (M i i)) + ∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
have h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n) := by
    rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
    · simp_rw [natDegree_X_sub_C]
      rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
    simp_rw [(monic_X_sub_C _).leadingCoeff]
    simp

Goal state after:
case neg
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
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i, (X - C (M i i)) + ∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
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
inst✝ : Nontrivial R
hn : Fintype.card n = 2
⊢ M.charpoly = X ^ 2 - C M.trace * X + C M.det

Tactic:
have : Nonempty n := by rw [← Fintype.card_pos_iff]; lia

Goal state after:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly = X ^ 2 - C M.trace * X + C M.det
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ↑((m + n).choose k)

Tactic:
cast_id

Goal state after:
m n k : ℕ
⊢ (m + n).choose k = (m + n).choose k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case zero
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
this : ∑ x, 1 = Fintype.card n
i : n
⊢ 0 - (C (M (c i) i)).coeff 0 ∈ I

Tactic:
coeff_C_zero,

Goal state after:
case zero
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
this : ∑ x, 1 = Fintype.card n
i : n
⊢ 0 - M (c i) i ∈ I
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
⊢ IsIntegral R x

Tactic:
by
  let A' : Subalgebra R A :=
    { carrier := { x | ∀ n ∈ N, x • n ∈ N }
      mul_mem' := fun {a b} ha hb n hn => smul_smul a b n ▸ ha _ (hb _ hn)
      one_mem' := fun n hn => (one_smul A n).symm ▸ hn
      add_mem' := fun {a b} ha hb n hn => (add_smul a b n).symm ▸ N.add_mem (ha _ hn) (hb _ hn)
      zero_mem' := fun n _hn => (zero_smul A n).symm ▸ N.zero_mem
      algebraMap_mem' := fun r n hn => (algebraMap_smul A r n).symm ▸ N.smul_mem r hn }
  let f : A' →ₐ[R] Module.End R N :=
    AlgHom.ofLinearMap
      { toFun := fun x => (DistribSMul.toLinearMap R M x).restrict x.prop
        map_add' := by intro x y; ext; exact add_smul _ _ _
        map_smul' := by intro r s; ext; apply smul_assoc }
      (by ext; apply one_smul)
      (by intro x y; ext; apply mul_smul)
  obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]
  have : Function.Injective f := by
    change Function.Injective f.toLinearMap
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro s hs
    have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
    exact Subtype.ext ((smul_eq_zero_iff_left ha₂).1 this)
  change IsIntegral R (A'.val ⟨x, hx⟩)
  rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this]
  have : Module.Finite R N := by rwa [Module.Finite.iff_fg]
  apply Algebra.IsIntegral.isIntegral

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
M : Matrix n n R
s : Finset n
⊢ (of (s.piecewise M.row (row 1))).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
by
  let e := Equiv.sumCompl (fun x => x ∈ s)
  let +generalize A : Matrix n n R := Matrix.of (s.piecewise M (1 : Matrix n n R))
  rw [← Matrix.det_submatrix_equiv_self e A]
  have h_blocks : A.submatrix e e =
      Matrix.fromBlocks
        (M.submatrix Subtype.val Subtype.val)
        (M.submatrix Subtype.val Subtype.val) 0 1 := by
    ext (i | i) (j | j) <;> dsimp [A, e]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_neg i.prop]
      exact Matrix.one_apply_ne (fun h => i.prop (h ▸ j.prop))
    · simp only [Finset.piecewise, if_neg i.prop, Matrix.one_apply, Subtype.ext_iff]
  rw [h_blocks, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one, mul_one]

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
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
| (D fun i ↦ (X • M.map ⇑C) i + 1 i).coeff k

Tactic:
show (fun i ↦ ((X : R[X]) • M.map C) i + (1 : Matrix n n R[X]) i) =
      (fun i => ((X : R[X]) • M.map C) i) + (fun i => (1 : Matrix n n R[X]) i) from rfl

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
| (D ((fun i ↦ (X • M.map ⇑C) i) + fun i ↦ 1 i)).coeff k
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p

Tactic:
have this t :
      (taylor x p).eval t =
      ∑ i ∈ Finset.range ((taylor x p).natDegree + 2), (taylor x p).coeff i * t ^ i :=
    (taylor x p).eval_eq_sum_range' (n := (taylor x p).natDegree + 2) (by lia) t
  rw [add_comm, ← p.taylor_eval x y, this, Finset.sum_range_succ', Finset.sum_range_succ']
  use ∑ i ∈ Finset.range p.natDegree, (taylor x p).coeff (i + 2) * y ^ i
  simp [pow_succ, mul_assoc, Finset.sum_mul]

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
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
s : Finset n
hs : s ∈ powersetCard k univ
⊢ (-1) ^ #s * (M.submatrix Subtype.val Subtype.val).det = (-1) ^ k * (M.submatrix Subtype.val Subtype.val).det

Tactic:
by rw [(Finset.mem_powersetCard.mp hs).2]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s))

Tactic:
rw [Finset.sum_congr rfl aux]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
m : M
a : A
⊢ (scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

Tactic:
by simp [scalarTensorEquiv]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
mn : M × N
r : R
⊢ (tensorEquiv R).symm (single mn r) = single mn.1 1 ⊗ₜ[R] single mn.2 r

Tactic:
by
  simp [tensorEquiv, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Tactic:
← top_le_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ⊤ ≤ integralClosure R A ↔ Algebra.IsIntegral R A
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = 0
⊢ f.Splits ∧ g.Splits

Tactic:
← hp,

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : (f * g).natDegree = 0
⊢ f.Splits ∧ g.Splits