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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
⊢ ∀ (c : B) (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x

Tactic:
intro c x
    obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x
    rfl

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
H : ∀ x ∈ adjoin R ↑σ, 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ 1 ⊗ₜ[R] (y * t) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
exact H _ h₃

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
⊢ ∀ (x y : A ⊗[R] (T ⧸ I)),
    (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (x * y) =
      (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) x *
        (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) y

Tactic:
by
    refine LinearMap.map_mul_of_map_mul_tmul fun a₁ a₂ b₁ b₂ ↦ ?_
    obtain ⟨b₁, rfl⟩ := Ideal.Quotient.mk_surjective b₁
    obtain ⟨b₂, rfl⟩ := Ideal.Quotient.mk_surjective b₂
    rw [← map_mul]
    simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, g,
      AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, ← Ideal.Quotient.mk_eq_mk,
      ← Algebra.TensorProduct.tmul_mul_tmul]
    rfl

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z) → ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Tactic:
rintro ⟨y, hy, z, hz⟩

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝

Tactic:
intro h s; exact h s

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

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s; exact h s

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Monoid R
S : Submonoid R
⊢ ((∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) →
    Nonempty (OreSet S)

Tactic:
· intro ⟨H, H'⟩
    choose r' s' h using H'
    exact ⟨H, r', s', h⟩

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 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)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ (algebraMap S (Localization.Away ↑r)).comp f =
    ((algebraMap S (Localization (Submonoid.powers ↑r))).comp (id S)).comp f

Tactic:
RingHom.comp_id

Goal state after:
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)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ (algebraMap S (Localization.Away ↑r)).comp f = (algebraMap S (Localization (Submonoid.powers ↑r))).comp f
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i

Tactic:
updateRow_self,

Goal state after:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ A i = A.updateRow j (A i) i
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
⊢ toLaurent p.reverse = invert (toLaurent p) * T ↑p.natDegree

Tactic:
by
  nontriviality R
  induction p using Polynomial.recOnHorner with
  | M0 => simp
  | MC _ _ _ _ ih => simp [add_mul, ← ih]
  | MX _ hp => simpa [natDegree_mul_X hp]

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 α
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card
  · have : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
    rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]
  replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le
  -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
  -- where `A'.det` is non-zero.
  let A' := mvPolynomialX n n ℤ
  suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, this]
  apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)
  calc
    A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
    _ = A'.det ^ Fintype.card n := by rw [mul_adjugate A', det_smul, det_one, mul_one]
    _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]

Goal state after:
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
⊢ ∑ j_1,
      (-1) ^ (↑j + ↑j_1) * A.updateRow j (Pi.single i 1) j j_1 *
        ((A.updateRow j (Pi.single i 1)).submatrix j.succAbove j_1.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
updateRow_self,

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * ((A.updateRow j (Pi.single i 1)).submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
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 α
inst✝ : StarRing α
⊢ A⁻¹ᴴ = Aᴴ⁻¹

Tactic:
rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]

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

Goal state before:
pp: case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal 0

Tactic:
Pi.zero_def,

Goal state after:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal fun x ↦ 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

pp: case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
· rw [nonsing_inv_nonsing_inv _ h]

Goal state after:
case neg
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.Charpoly.Basic

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

Tactic:
charpoly,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.map ⇑f).charmatrix.det = Polynomial.map f M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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

Tactic:
charpoly,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.charmatrix.map ⇑(mapRingHom f)).det = (mapRingHom f) M.charmatrix.det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-((scalar m) X - (A * B).map ⇑C)).det * (-(scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)

Tactic:
det_neg

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-1) ^ Fintype.card m * ((scalar m) X - (A * B).map ⇑C).det * (-(scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

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

Tactic:
intro L₁ L₂ E PE

Goal state after:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
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
⊢ (toFunLinear n R A) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    (toFunLinear n R A) (a₁✝ ⊗ₜ[R] b₁✝) * (toFunLinear n R A) (a₂✝ ⊗ₜ[R] b₂✝)

Tactic:
toFunLinear,

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
⊢ (TensorProduct.lift (toFunBilinear n R A)) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    (TensorProduct.lift (toFunBilinear n R A)) (a₁✝ ⊗ₜ[R] b₁✝) *
      (TensorProduct.lift (toFunBilinear n R A)) (a₂✝ ⊗ₜ[R] b₂✝)
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
⊢ (toFunLinear n R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
toFunLinear,

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
⊢ (TensorProduct.lift (toFunBilinear n R A)) (1 ⊗ₜ[R] 1) = 1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ X ^ (Fintype.card n - Fintype.card Unit) * (replicateRow Unit v * replicateCol Unit u).charpoly =
    X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
charpoly,

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : Nonempty n
h : 1 ≤ Fintype.card n
⊢ X ^ (Fintype.card n - Fintype.card Unit) * (replicateRow Unit v * replicateCol Unit u).charmatrix.det =
    X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
⊢ (M - (scalar n) μ).charpoly = M.charpoly.comp (X + C μ)

Tactic:
charpoly,

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
⊢ (M - (scalar n) μ).charmatrix.det = M.charmatrix.det.comp (X + C μ)
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
h : Represents b A f
i : ι
this : ((PiToModule.fromMatrix R b) A) (Pi.single i 1) = ((PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1, A i_1 i • b i_1 = f (b i)

Tactic:
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this

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
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < ↑(Fintype.card n - 1)

Tactic:
charpoly,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (M.charmatrix.det - ∏ i, (X - C (M i i))).degree < ↑(Fintype.card n - 1)
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
hp : p.FG
⊢ p.generators.Finite

Tactic:
rw [← Cardinal.lt_aleph0_iff_set_finite, Submodule.generators_card]
  exact spanRank_finite_iff_fg.mpr hp

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
m : M
hm : m ≠ 0
this : (R ∙ m).spanFinrank < 1
⊢ False

Tactic:
simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this

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
M : Matrix n n R
a✝ : Nontrivial R
h : Fintype.card n = 0
⊢ M.charpoly.Monic

Tactic:
charpoly,

Goal state after:
case pos
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
⊢ M.charmatrix.det.Monic
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ IsIntegral R (f b)

Tactic:
IsIntegral,

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ (algebraMap R C).IsIntegralElem (f b)
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
⊢ M.det = (-1) ^ Fintype.card n * eval 0 M.charpoly

Tactic:
charpoly,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1) ^ Fintype.card n * eval 0 M.charmatrix.det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = eval 0 (1 + X • M.map ⇑C).det

Tactic:
eval_det_add_X_smul,

Goal state after:
case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = eval 0 (det 1)
Module: Mathlib.Algebra.Polynomial.Lifts

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

Tactic:
coeff_monomial,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
⊢ ∀ (a : ℕ), (∑ x ∈ p.support, if x = a then g x else 0) ≠ 0 ↔ p.coeff a ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
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) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

Tactic:
· rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]
    split_ifs with m0 mp <;> simp_all

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det =
    C A⁻¹.det * (C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det)

Tactic:
by ac_rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support

Tactic:
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
⊢ (C a * X + C b).Splits

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
b : R
hf : (C 0 * X + C b).natDegree ≤ 1
h : Invertible (C 0 * X + C b).leadingCoeff
⊢ (C 0 * X + C b).Splits

case inr
R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
ha : a ≠ 0
⊢ (C a * X + C b).Splits
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0

Tactic:
by
  ext i
  simp

Goal state after: