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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)

Tactic:
simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑((AlgebraTensorModule.lTensor S M) N.subtype)
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
s : Set S
spn : Ideal.span s = ⊤
Mₛ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₛ r)
inst✝³ : (r : ↑s) → Module R (Mₛ r)
inst✝² : (r : ↑s) → Module S (Mₛ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Mₛ r)
g : (r : ↑s) → M →ₗ[S] Mₛ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
H :
  ∀ (r : ↑s) ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor (Mₛ r) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)

Tactic:
simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
s : Set S
spn : Ideal.span s = ⊤
Mₛ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₛ r)
inst✝³ : (r : ↑s) → Module R (Mₛ r)
inst✝² : (r : ↑s) → Module S (Mₛ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Mₛ r)
g : (r : ↑s) → M →ₗ[S] Mₛ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
H :
  ∀ (r : ↑s) ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor (Mₛ r) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑((AlgebraTensorModule.lTensor S M) N.subtype)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap f ↑r)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R),
      Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap f ↑r)) → P f

Tactic:
apply forall₅_congr

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S),
      Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f

Tactic:
apply forall₅_congr

Goal state after:
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
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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
let := e.symm.toRingHom.toAlgebra

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this : Algebra S R := e.symm.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
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 : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this : Algebra S R := e.symm.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
have : IsLocalization.Away (1 : S) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.symm.bijective

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝ : Algebra S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
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 : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this : Algebra S T := e.toRingHom.toAlgebra
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
have : IsLocalization.Away (1 : S) T :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
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
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P ((IsLocalization.map (Localization.Away ↑⟨f r, ⋯⟩) f ?m.175).comp (algebraMap R (Localization.Away r)))

pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
· apply hP' _ r
    exact hs' ⟨r, hr⟩

Goal state after:
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
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D

Tactic:
rw [fromBlocks_transpose, hA, hCB, hBC, hD]

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

Goal state before:
pp: case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i ↦ ∏ j ∈ univ.erase i, v j) i j

Tactic:
· rw [diagonal_apply_ne _ hij]
    refine det_eq_zero_of_row_eq_zero j fun k => ?_
    obtain rfl | hjk := eq_or_ne k j
    · rw [updateCol_self, Pi.single_eq_of_ne' hij]
    · rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
⊢ LinearIndependent R fun i ↦ r * ↑s ^ ↑i

Tactic:
refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    simpa only [dif_pos i.prop] using this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0
      (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop

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 α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ A⁻¹.det = A.det⁻¹ʳ

case neg.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : Nonempty n
⊢ A⁻¹.det = A.det⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
· simpa only [Classical.not_not] using h

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

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : ¬IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case neg.inl
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✝ : IsEmpty n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

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
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
H : ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
by
  rcases H with ⟨L₀, L₀', D₀, h₀⟩
  refine ⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩
  have : M = reindexAlgEquiv 𝕜 _ e.symm (reindexAlgEquiv 𝕜 _ e M) := by simp
  rw [this]
  simp_rw [List.map_map, toMatrix_reindexEquiv_prod, ← map_mul, h₀]
  simp

Goal state after:
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
h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv M.charmatrix.adjugate * (X - C M)
⊢ (aeval M) M.charpoly = 0

Tactic:
apply_fun fun p => p.eval M at h

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
h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))
⊢ (aeval M) M.charpoly = 0
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 α
C : Matrix n m α
D : Matrix n n α
⊢ IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

Tactic:
by
  simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
    (fromBlocksZero₁₂InvertibleEquiv _ _ _).nonempty_congr]

Goal state after:
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
u v : n → R
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : IsEmpty n
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

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
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P

Tactic:
rw [← commute_X P]

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
isUnit_iff_coeff_isUnit_isNilpotent,

Goal state after:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ (IsUnit ((C r + X * P).coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent ((C r + X * P).coeff i)) ↔ IsUnit r ∧ IsNilpotent P
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
⊢ p.spanRank < ℵ₀ ↔ p.FG

Tactic:
by
  rw [spanRank, Submodule.fg_def]
  constructor
  · rintro h
    obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
    refine ⟨s.1, ?_, s.2⟩
    simpa [← hs] using h
  · rintro ⟨s, hs₁, hs₂⟩
    exact (ciInf_le' _ ⟨s, hs₂⟩).trans_lt (by simpa)

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

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ↑p.generators.ncard = ↑p.spanFinrank

Tactic:
← fg_iff_spanRank_eq_spanFinrank.mpr h,

Goal state after:
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.spanRank
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.trace = -M.charpoly.nextCoeff

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h✝ : IsEmpty n
⊢ M.trace = -M.charpoly.nextCoeff

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h✝ : Nonempty n
⊢ M.trace = -M.charpoly.nextCoeff
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
s : Set A
hfs : s.Finite
his : ∀ x ∈ s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG

Tactic:
induction s, hfs using Set.Finite.induction_on with
  | empty =>
    refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
  | @insert a s _ _ ih =>
    rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Goal state after:
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
k : ℕ
h : g k = 0
⊢ p.coeff k = 0

Tactic:
← hg,

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
k : ℕ
h : g k = 0
⊢ f (g k) = 0
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
a✝ : Nontrivial R
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace
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
hM : IsNilpotent M
⊢ IsNilpotent M.trace

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic

Tactic:
rw [hmg]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)))).prod.Monic
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
⊢ f.nextCoeff = -f.roots.sum

Tactic:
by
  simp [hf.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, hm]

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'

Tactic:
← hg,

Goal state after:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ (Ideal.Quotient.mkₐ S I) g' = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
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
h : Algebra.IsIntegral R T
⊢ ∀ (x : T), IsIntegral S x

Tactic:
by
    apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)
    rw [← IsScalarTower.algebraMap_eq R S T]
    exact h.isIntegral

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
⊢ FaithfullyFlat R M ↔
    Flat R M ∧
      ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)

Tactic:
refine ⟨fun fl => ⟨inferInstance, rTensor_nontrivial R M⟩, fun ⟨flat, faithful⟩ => ⟨?_⟩⟩

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤