mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝¹ x✝ : WalkingReflexivePair
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝¹ with
      | zero => e₀
      | one => e₁) ≫
      G.map f

Tactic:
by
    cases f
    all_goals
      dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁸ : CommSemiring A
B : Type u_3
inst✝⁷ : CommSemiring B
C : Type u_4
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst✝¹ : 𝔓.LiesOver P
inst✝ : P.LiesOver p
⊢ under A P = under A 𝔓

Tactic:
𝔓.over_def P,

Goal state after:
A : Type u_2
inst✝⁸ : CommSemiring A
B : Type u_3
inst✝⁷ : CommSemiring B
C : Type u_4
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst✝¹ : 𝔓.LiesOver P
inst✝ : P.LiesOver p
⊢ under A (under B 𝔓) = under A 𝔓
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
hp : 𝔓.LiesOver p
hP : 𝔓.LiesOver P
⊢ under A 𝔓 = under A P

Tactic:
𝔓.over_def P,

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
hp : 𝔓.LiesOver p
hP : 𝔓.LiesOver P
⊢ under A 𝔓 = under A (under B 𝔓)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
⊢ map f M' ≤ localized₀ p f M'

Tactic:
rintro - ⟨x, hx, rfl⟩

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ f x ∈ localized₀ p f M'
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
this : Module (Localization p) N := IsLocalizedModule.module p f
⊢ localized₀ p f (⨆ i, g i) = ⨆ i, localized₀ p f (g i)

Tactic:
have : IsScalarTower R (Localization p) N := IsLocalizedModule.isScalarTower_module p f

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
this✝ : Module (Localization p) N := IsLocalizedModule.module p f
this : IsScalarTower R (Localization p) N
⊢ localized₀ p f (⨆ i, g i) = ⨆ i, localized₀ p f (g i)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid 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✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
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
M'✝ M' : Submodule R M
x : ↥p
m : N ⧸ localized' S p f M'
⊢ ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x) (IsLocalization.mk' S 1 x • m) = m

Tactic:
rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (I ^ n)) x) ↔ IsUnit ((mk I) x)

Tactic:
rw [← IsNilpotent.isUnit_quotient_mk_iff (I := Ideal.map (Ideal.Quotient.mk (I ^ n)) I)]

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)

Tactic:
choose r' s' h using H

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)
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 : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := ⋯
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (IsLocalization.Away.map R T f 1).comp (algebraMap R R)

Tactic:
IsLocalization.Away.map,

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 : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := e.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (IsLocalization.map T f ⋯).comp (algebraMap R R)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
⊢ A.IsSymm

Tactic:
← A.conjTranspose_conjTranspose

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
⊢ Aᴴᴴ.IsSymm
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ Finset.univ.card • 1 ≤ Fintype.card n

Tactic:
simp [mul_one, Finset.card_univ]

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 α
⊢ IsLinearMap α A.cramerMap

Tactic:
by
  constructor <;> intros <;> ext i
  · apply (cramerMap_is_linear A i).1
  · apply (cramerMap_is_linear A i).2

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
⊢ adjugate 1 = 1

Tactic:
ext
  simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

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
M : Matrix n n R
h : M ∈ Set.range ⇑(scalar n)
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Tactic:
rw [mem_range_scalar_iff_commute_single] at h

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M
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
⊢ A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
  rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
  rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

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

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : ⅟C * A = B
⊢ A = C * B

Tactic:
rw [← h, Matrix.mul_invOf_cancel_left]

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 α
i : n
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
have : Nonempty n := ⟨i⟩

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
⊢ A.det = ∑ j, A i j * A.adjugate j i
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
by
  have : Nonempty n := ⟨i⟩
  obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)
  obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
  let A' := reindex e e A
  suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i) by
    simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
      Equiv.symm_apply_apply] at this
    exact this
  rw [det_succ_row A' (e i)]
  simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]

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

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ includeLeft A.det ^ Fintype.card n * includeRight B.det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,
    _root_.mul_one, _root_.one_mul]

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

Goal state before:
pp: case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ (A * A ^ k).adjugate = A.adjugate ^ (k + 1)

Tactic:
adjugate_mul_distrib,

Goal state after:
case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ (A ^ k).adjugate * A.adjugate = A.adjugate ^ (k + 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
⊢ ((reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · convert! h.submatrix
    simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]
  · convert! h.submatrix
    simp only [comp_assoc b e e.symm, Equiv.self_comp_symm, comp_id]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A.det * B.det)⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)

Tactic:
adjugate_mul_distrib,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A.det * B.det)⁻¹ʳ • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (matPolyEquiv (p • 1)).coeff m i j = (Polynomial.map (algebraMap R (Matrix n n R)) p).coeff m i j

Tactic:
simp only [matPolyEquiv_coeff_apply, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul, mul_ite,
    mul_one, mul_zero, coeff_map, algebraMap_matrix_apply, Algebra.algebraMap_self,
    RingHom.id_apply]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ ((List.map toMatrix []).prod * M * (List.map toMatrix []).prod) i j = diagonal (fun x ↦ 1) i j

Tactic:
exact hn.elim' i

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
hf : Function.Injective ⇑f
s : Set M
hs : Cardinal.mk ↑(⇑f '' s) = (map f (span R s)).spanRank
e : span S (⇑f '' s) = map f (span R s)
⊢ Cardinal.lift.{v, u} (span R s).spanRank ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank

Tactic:
grw [← hs, Cardinal.mk_image_eq_lift _ _ hf, Cardinal.lift_le, spanRank_span_le_card]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Submodule.spanFinrank (map f I) = Submodule.spanFinrank I

Tactic:
by
  rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]

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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ ∑ b, (Equiv.Perm.sign b • ∏ i, M.charmatrix (b i) i).coeff k ∈ I ^ (Fintype.card n - k)

Tactic:
apply sum_mem

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ ∀ c ∈ univ, (Equiv.Perm.sign c • ∏ i, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
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 : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
by
  rcases subsingleton_or_nontrivial S with hR | hR
  · obtain rfl : p = 1 := Subsingleton.elim _ _
    exact ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
  obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
  exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

Goal state after:
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
A' : Subalgebra R A := ⋯
x✝ : ↥N
⊢ ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } 1) x✝) = ↑(1 x✝)

Tactic:
apply one_smul

Goal state after:
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), n.choose i ^ 2 = ∑ ij ∈ antidiagonal n, n.choose ij.1 * n.choose ij.2

Tactic:
sum_antidiagonal_eq_sum_range_succ_mk

Goal state after:
n : ℕ
⊢ ∑ i ∈ range (n + 1), n.choose i ^ 2 = ∑ k ∈ range n.succ, n.choose (k, n - k).1 * n.choose (k, n - k).2
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
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
⊢ ∀ (x y : ↥A'),
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
        { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
intro x y; ext; apply mul_smul

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(0! • hasseDeriv 0) = (⇑derivative)^[0]

Tactic:
hasseDeriv_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(0! • LinearMap.id) = (⇑derivative)^[0]
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ eval r ((hasseDeriv 0) f) = eval r f

Tactic:
hasseDeriv_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ eval r (LinearMap.id f) = eval r f
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
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
h_set : {s | #s = k} = powersetCard k univ
⊢ ∑ a ∈ powersetCard k univ, det (a.piecewise M 1) =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
exact Finset.sum_congr rfl fun s _ => det_piecewise_one_eq_submatrix_det M s

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
⊢ M.charpoly.coeff (Fintype.card n - k) =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
rw [hrev, M.reverse_charpoly]

Goal state after:
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
⊢ M.charpolyRev.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
⊢ eval₂ f (f r) (p.scaleRoots s) = 0

Tactic:
nontriviality S using Subsingleton.eq_zero (α := S)
  convert! @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
  rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]
  exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n

Tactic:
simp [coeff_map]

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

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : (C f.leadingCoeff).degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) 0).prod
⊢ ∃ a, eval a f = 0

Tactic:
degree_C hf₀

Goal state after:
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : 0 ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) 0).prod
⊢ ∃ a, eval a f = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (a ::ₘ m)).prod
ha : a ∈ a ::ₘ m
⊢ eval a f = 0

Tactic:
by rw [hm]; simp

Goal state after:
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
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
by
  obtain ⟨_, hb₁, hb₂⟩ := integerNormalization_spec M p
  let := isDomain_of_le_nonZeroDivisors S hM
  let := (faithfulSMul_iff_algebraMap_injective R S).mpr <| IsLocalization.injective S hM
  let : Function.Injective <| mapRingHom (algebraMap R S) := by
    rw [coe_mapRingHom, map_injective_iff]
    exact IsLocalization.injective S hM
  rw [← _root_.map_eq_zero_iff (mapRingHom (algebraMap R S)) this, coe_mapRingHom, hb₂]
  exact smul_eq_zero_iff_right <| nonZeroDivisors.ne_zero (hM hb₁)

Goal state after: