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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit (mk' (Localization.AtPrime J) (f r) ⟨f ↑s, ⋯⟩)
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Tactic:
rw [AtPrime.isUnit_mk'_iff] at hx ⊢

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : f r ∈ J.primeCompl
⊢ r ∈ I.primeCompl
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝³ : a ∈ s
b : S
a✝² : b ∈ s
a✝¹ : b ∉ P
c : S
a✝ : c ∈ s
⊢ ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
d

Goal state after:
case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝³ : a ∈ s
b : S
a✝² : b ∈ s
a✝¹ : b ∉ P
c : S
a✝ : c ∈ s
d : S
⊢ d ∈ s → d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
obtain ⟨t, ⟨htP, -⟩, ht⟩ := H.ge (Set.mem_univ x)

Goal state after:
case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝⁵ : a ∈ s
b : S
a✝⁴ : b ∈ s
a✝³ : b ∉ P
c : S
a✝² : c ∈ s
d : S
a✝¹ : d ∈ s
a✝ : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
t : S
ht : t * x ∈ s
htP : t ∈ ↑P.primeCompl
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
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:
refine LinearMap.map_mul_of_map_mul_tmul fun a₁ a₂ b₁ b₂ ↦ ?_

Goal state after:
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)) ⋯
a₁ a₂ : A
b₁ b₂ : T ⧸ I
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] b₂)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ Aᵀ.IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.transpose)⟩

Goal state after:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : Aᵀ.IsSymm
⊢ A.IsSymm
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ a ∉ p.coeff.support → (Finsupp.single a (p.coeff a)) a = 0

Tactic:
intro ha
    rw [single_eq_same, notMem_support_iff.mp ha]

Goal state after:
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
inst✝ : IsFractionRing S A
⊢ finrank R S = finrank R A

Tactic:
nontriviality R
  classical
  apply Cardinal.toNat_eq_of_forall_le_iff
  intro n
  simp_rw [Module.le_rank_iff_exists_finset, LinearIndepOn]
  constructor
  · rintro ⟨s, rfl, hs⟩
    let f : S ↪ A := ⟨algebraMap S A, FaithfulSMul.algebraMap_injective S A⟩
    exact ⟨s.map f, s.card_map f,
      (linearIndependent_equiv (s.equivMap f)).mp (LinearIndependent.algebraMap_comp_iff.mpr hs)⟩
  · rintro ⟨s, rfl, hs⟩
    exact ⟨finsetIntegerMultiple S⁰ s, card_finsetIntegerMultiple S⁰ s,
      linearIndepOn_finsetIntegerMultiple S⁰ hs⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
⊢ ∃ s, #↑s = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
obtain ⟨w, hw⟩ :=
    IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) <|
      Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M)
        |>.linearIndependent.restrict_scalars' _

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ ∃ s, #↑s = Module.rank R M ∧ LinearIndepOn R id s
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
by_cases hb : j = b

Goal state after:
case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

case neg
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : ¬j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
m : Type u_4
a : n
b : m
ha : a ≠ i
c : R
M : Matrix n m R
⊢ (transvection i j c * M) a b = M a b

Tactic:
simp [transvection, Matrix.add_mul, ha]

Goal state after:
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
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L).prod * (List.map toMatrix L.reverse).prod = 1

Tactic:
rw [← reverse_inv_prod_mul_prod L.reverse, L.reverse_reverse]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))

Tactic:
rw [← lift_lift.{max uS uT, max uM uN}, ← lift_umax.{uP},
    ← IsLocalizedModule.lift_rank_eq pT (mk T ST P 1) hpT,
    ← IsLocalization.rank_eq ST pT hpT, lift_id'.{uP, max uS uT},
    ← lift_id'.{max uS uT, max uS uT uP} (Module.rank ..), lift_lift,
    ← lift_lift.{max uS uT uN, uM}, lift_inj]

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uS uT uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P)) =
    Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N))
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case MC
R : Type u_3
inst✝ : CommSemiring R
a✝³ : Nontrivial R
p✝ : R[X]
a✝² : R
a✝¹ : p✝.coeff 0 = 0
a✝ : a✝² ≠ 0
ih : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ + Polynomial.C a✝²).reverse =
    invert (toLaurent (p✝ + Polynomial.C a✝²)) * T ↑(p✝ + Polynomial.C a✝²).natDegree

Tactic:
simp [add_mul, ← ih]

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
M✝ : Matrix n n α
⊢ ((evalRingHom 0).mapMatrix (g M✝)).adjugate = M✝.adjugate

Tactic:
f'_inv

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

Tactic:
f'_inv

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 N : Matrix n n α
⊢ M * N = M * N
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ Function.Injective fun v ↦ v ᵥ* Aᵀ

Tactic:
vecMul_transpose

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 * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
    simp [listTransvecRow, listTransvecCol_mul_last_row]
  rw [this]
  apply mul_listTransvecRow_last_row
  simpa [listTransvecCol_mul_last_row] using hM

Goal state after:
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 α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val✝ : Invertible A
ih : Invertible (C + C * V * A⁻¹ * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv] at ih

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val✝ : Invertible A
ih : Invertible (C + C * V * ⅟A * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg.inr
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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = 0

Tactic:
nonsing_inv_apply_not_isUnit _ hAB

Goal state after:
case neg.inr
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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg.inr
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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = 0

Tactic:
nonsing_inv_apply_not_isUnit _ hAB

Goal state after:
case neg.inr
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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ 0 = 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
M : Matrix n n R
i : n
⊢ M.charmatrix i i = X - C (M i i)

Tactic:
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply,
    diagonal_apply_eq]

Goal state after:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ b' + a < b' + b

Tactic:
gcongr

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }

Tactic:
obtain ⟨z, hz⟩ := @powSubPowFactor x y (k + 1)
    exists z * x + y ^ (k + 1)
    linear_combination (norm := ring) x * hz

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ w ^ 2 * z ^ 2

Tactic:
gcongr

Goal state after:
case a
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ z ∣ z ^ 2
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
  simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
  simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero,
    ← Polynomial.isNilpotent_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
a✝ : IsUnit (p.coeff 0)
⊢ ¬p.coeff p.natDegree = 0

Tactic:
contrapose! hpl

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
a✝ : IsUnit (p.coeff 0)
hpl : p.coeff p.natDegree = 0
⊢ p.natDegree ≤ 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Ring T
f : R →+* S
g : S →+* T
x : T
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) x p = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
simpa only [eval₂_eq_eval_map, map_map] using hx

Goal state after:
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:
rw [IsIntegral, ← ((AlgHomClass.toAlgHom f).restrictScalars R).comp_algebraMap]

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
⊢ ((↑(AlgHom.restrictScalars R ↑f)).comp (algebraMap R B)).IsIntegralElem (f b)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ
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
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (1 + k) ∈ 1

Tactic:
Ideal.one_eq_top

Goal state after:
case succ
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
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (1 + k) ∈ ⊤
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ (taylor r) ((taylor s) f) = (taylor (r + s)) f

Tactic:
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, add_assoc]

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

Goal state before:
pp: case inr.inr.cons
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ (((X + C a) ::ₘ Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits

Tactic:
Multiset.prod_cons,

Goal state after:
case inr.inr.cons
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ (((X + C a) * (Multiset.map (fun x ↦ X + C x) s).prod).scaleRoots r).Splits
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
x : A
hx : IsIntegral R x
⊢ {x} ⊆ ↑(integralClosure R A)

Tactic:
simp only [SetLike.mem_coe, Set.singleton_subset_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ x ∈ integralClosure R A
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = C f.leadingCoeff * ((X - C a) ::ₘ Multiset.map (fun x ↦ X - C x) f.roots).prod
⊢ f.Splits

Tactic:
Multiset.prod_cons,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = C f.leadingCoeff * ((X - C a) * (Multiset.map (fun x ↦ X - C x) f.roots).prod)
⊢ f.Splits
Module: Mathlib.RingTheory.Localization.Integral

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
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ (aeval x) (integerNormalization M p) = 0

Tactic:
by
  rwa [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M
I : Ideal R
⊢ I ≠ ⊤ → I • ⊤ ≠ ⊤ ↔ I • ⊤ = ⊤ → I = ⊤

Tactic:
by tauto

Goal state after: