mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
by rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.hom_inv_id_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
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ map (algebraMap A D) (under A P) ≤ map (algebraMap B D) P

Tactic:
map_le_iff_le_comap,

Goal state after:
A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ under A P ≤ comap (algebraMap A D) (map (algebraMap B D) P)
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, map S.mkQ (a✝¹ ^ n • ⊤) ≤ ⊥

Tactic:
map_le_iff_le_comap,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ comap S.mkQ ⊥
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'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ localized' S p f M' ≤ N'

Tactic:
localized'_eq_span,

Goal state after:
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'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ span S (⇑f '' ↑M') ≤ N'
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
s : Set M
⊢ localized' S p f (span R s) = span S (⇑f '' s)

Tactic:
localized'_eq_span,

Goal state after:
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
s : Set M
⊢ span S (⇑f '' ↑(span R s)) = span S (⇑f '' s)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I ≤ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I)

pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
· simp only [le_iInf₂_iff, ← Ideal.map_le_iff_le_comap, le_refl, implies_true]

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : 0 = 1
⊢ False

Tactic:
by
    rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
    obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze
    have htz : (t : R) = 0 := by simpa using ht.symm
    exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ x - x + 1 = 1

Tactic:
sub_self,

Goal state after:
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ 0 + 1 = 1
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ y - y + 1 = 1

Tactic:
sub_self,

Goal state after:
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ 0 + 1 = 1
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 : S →+* T
e : R ≃+* S
hf : P f
this✝ : Algebra R S := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 S
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
exact hP.left S (1 : R) f hf

Goal state after:
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
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree

Tactic:
rcases Int.units_eq_one_or (sign g) with sg | sg

Goal state after:
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = 1
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree

case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = -1
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree
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
a✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R S ↔ ↑n ≤ Module.rank R A

Tactic:
simp_rw [Module.le_rank_iff_exists_finset, LinearIndepOn]

Goal state after:
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
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) ↔
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (C a * T n).coeff.support ⊆ {n}

Tactic:
rw [← single_eq_C_mul_T]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support ⊆ {n}
Module: Mathlib.Algebra.Polynomial.Laurent

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

Tactic:
rw [← single_eq_C_mul_T]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support = {n}
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ∃ r s, ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
obtain ⟨r, s, h⟩ := hS

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) = diagonal (fun mn ↦ f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]

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

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : (fun x ↦ A * x) B = (fun x ↦ A * x) C
⊢ B = C

Tactic:
refine hA.matrix ?_

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : (fun x ↦ A * x) B = (fun x ↦ A * x) C
⊢ (fun x ↦ A.det • x) B = (fun x ↦ A.det • x) C
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B = C

Tactic:
refine hA.matrix ?_

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ (fun x ↦ A.det • x) B = (fun x ↦ A.det • x) C
Module: Mathlib.LinearAlgebra.Matrix.Invertible

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

Tactic:
sub_eq_self,

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A.det
⊢ ⅟A.det • (A.adjugate * A) = 1

Tactic:
adjugate_mul,

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A.det
⊢ ⅟A.det • A.det • 1 = 1
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
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ f' (g (A * B)).adjugate = f' ((g B).adjugate * (g A).adjugate)

Tactic:
←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left,

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
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ f' (g (A * B)).adjugate = f' (g A * g B).adjugate
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 * (A.adjugate * A).adjugate = A * A.det ^ (Fintype.card n - 1) • 1

Tactic:
adjugate_mul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A * (A.det • 1).adjugate = A * A.det ^ (Fintype.card n - 1) • 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M - N) i j = 0

Tactic:
Matrix.sub_apply,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ M i j - N i j = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (↑h.unit⁻¹ * N * ↑h.unit).det = N.det

Tactic:
det_units_conj'

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ N.det = N.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
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n : ℕ
⊢ span R ↑{1} = M ^ Nat.zero

Tactic:
by simp [one_eq_span]

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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x, 1 = Fintype.card n

Tactic:
rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]

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

Goal state before:
pp: m n k : ℕ
⊢ ((X + 1) ^ m * (X + 1) ^ n).coeff k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

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 :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
h' : ∀ a ∈ N, a = 0
⊢ False

Tactic:
apply hN

Goal state after:
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 := ⋯
f : ↥A' →ₐ[R] Module.End R ↥N := ⋯
h' : ∀ a ∈ N, a = 0
⊢ N = ⊥
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))
Module: Mathlib.Algebra.Polynomial.Taylor

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

Tactic:
taylor_apply,

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

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

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
s : S
⊢ (tensorEquivSum R σ ι S) (C s ⊗ₜ[R] C r) = C (r • s)

Tactic:
simp [tensorEquivSum, algebraTensorAlgEquiv, sumAlgEquiv, renameEquiv, rename, C, monomial,
    mul_comm]

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

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

Tactic:
simp [tensorEquiv, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

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]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ Polynomial.map (algebraMap R S) (integerNormalization M p) = 0 ↔ p = 0

Tactic:
hb₂

Goal state after:
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]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ w✝ • p = 0 ↔ p = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
x : S
⊢ (aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.aroots S)).prod

Tactic:
simp [← eval_map_algebraMap, hf.eval_eq_prod_roots]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : (IsLocalization.map Sₘ (algebraMap R S) ⋯) v' * (algebraMap S Sₘ) ((algebraMap R S) ↑⟨v, ⋯⟩) = 1
⊢ (algebraMap Rₘ Sₘ) v' * (algebraMap S Sₘ) u = 1

Tactic:
exact hv.2 ▸ hv'

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)

Tactic:
obtain ⟨p, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) s

Goal state after:
case refine_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) s p = 0
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)