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

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
⊢ (equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)) =
    (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹

Tactic:
by
  have h₁ : Ideal.Quotient.mk p ↑s ≠ 0 := by
    simpa [ne_eq, Ideal.Quotient.eq_zero_iff_mem] using Ideal.mem_primeCompl_iff.mp s.prop
  have h₂ : equivQuotMaximalIdeal p Rₚ (Ideal.Quotient.mk p ↑s) ≠ 0 := by
    rwa [RingEquiv.map_ne_zero_iff]
  rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotMaximalIdeal_apply_mk, ← map_mul,
    mk'_spec, Ideal.Quotient.mk_algebraMap, equivQuotMaximalIdeal_apply_mk,
    Ideal.Quotient.mk_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.toRingHom = g.toRingHom
⊢ f = g

Tactic:
by ext; exact RingHom.congr_fun this _

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H : ∀ {R : Type u} [inst : CommRing R] (M : Submonoid R), P (algebraMap R (Localization M))
⊢ HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  introv R _
  rw [← (IsLocalization.algEquiv M (Localization M) S).toAlgHom.comp_algebraMap]
  exact hP.1 _ _ (H _)

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
⊢ P f

Tactic:
let := f.toAlgebra
  have := IsLocalization.of_le_isUnit (S := .powers (1 : R)) (by simp)
  have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R))
    (AlgEquiv.ofBijective (Algebra.ofId R S) hf)
  exact H _ 1

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑(c * s) * x ∈ pS

Tactic:
Submonoid.coe_mul,

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * ↑s * x ∈ pS
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
hf : P f
⊢ IsLocalization (Submonoid.powers (f r)) S'

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
RingHom.comp_apply,

Goal state after:
case h
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n) = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
coeff_det_X_add_C_card

Goal state after:
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : det 1 = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[T;T⁻¹]
h : ∀ (a : ℤ), p.coeff a = q.coeff a
a✝ : ℤ
⊢ p.coeff a✝ = q.coeff a✝

Tactic:
exact h _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ f.degree = ⊥ ↔ f = 0

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, degree_zero]⟩

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
⊢ f = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if j' = j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Tactic:
← dite_eq_ite,

Goal state after:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if x : j' = j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * T ↑n = toLaurent p * T (-↑n) * T ↑n

Tactic:
mul_T_assoc,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ IsLocalization.mk' R[T;T⁻¹] p ⟨X ^ n, ⋯⟩ * T ↑n = toLaurent p * T (-↑n + ↑n)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
by_cases ha : e t_i = a

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul 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✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{max uP uM, max uP uT} (Module.rank T (FT ⊗[T] P)) = Cardinal.lift.{max uP uT, uM} (Module.rank R M)

Tactic:
← lift_lift.{uM},

Goal state after:
case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul 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✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{uP, max uM uP uT} (Cardinal.lift.{uM, max uP uT} (Module.rank T (FT ⊗[T] P))) =
    Cardinal.lift.{max uP uT, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : β), (f 0) x = 0

pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), (f x) 0 = 0

Tactic:
· intro; exact LinearMap.map_zero₂ _ _

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), (f x) 0 = 0
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 α
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
let g : Matrix n n α → Matrix n n α[X] := fun M =>
    M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])
  let f' : Matrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix
  have f'_inv : ∀ M, f' (g M) = M := by
    intro
    ext
    simp [f', g]
  have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
    intro
    rw [RingHom.map_adjugate, f'_inv]
  have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N := by
    intro M N
    rw [map_mul, f'_inv, f'_inv]
  have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
    intro M
    refine Polynomial.Monic.isRegular ?_
    simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
  rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_mul]

Goal state after:
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 α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (⅟(diagonal v).det • (diagonal v).adjugate.diag * v) i = 1 i

Tactic:
adjugate_diagonal,

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 α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (⅟(diagonal v).det • (diagonal fun i ↦ ∏ j ∈ univ.erase i, v j).diag * v) i = 1 i
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 α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (v * ⅟(diagonal v).det • (diagonal v).adjugate.diag) i = 1 i

Tactic:
adjugate_diagonal,

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 α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (v * ⅟(diagonal v).det • (diagonal fun i ↦ ∏ j ∈ univ.erase i, v j).diag) i = 1 i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0

Tactic:
· contrapose! H
      rintro ⟨⟩ j
      exact (H j).2

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ eval₂ (RingHom.id R) r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
← coe_eval₂RingHom,

Goal state after:
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ (eval₂RingHom (RingHom.id R) r) M.det = (eval ((scalar n) r) (matPolyEquiv M)).det
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + a
⊢ a' = b'

Tactic:
rw [p] at H

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Add α
inst✝ : IsRightCancelAdd α
p : a = b
H : a' + b = b' + b
⊢ a' = b'
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
obtain ⟨n, hn⟩ := hnil

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
k : ℕ
⊢ C r ^ k = 0 ↔ r ^ k = 0

Tactic:
simpa only [← C_pow] using C_eq_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    ((PiToModule.fromEnd R b) f ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1

Tactic:
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
      PiToModule.fromMatrix_apply_single_one]

Goal state after:
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ∑ i, A i i✝ • b i = f (b i✝)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ (PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 0

Tactic:
rw [map_zero, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0

Tactic:
assumption

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ IsIntegral R ((algebraMap A B) x)

Tactic:
use f, hf

Goal state after:
case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) f = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, 0) = 0

Tactic:
Prod.zero_eq_mk

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (0, 0) = (0, 0)
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ((X + 1) ^ (m + n)).coeff k

Tactic:
rw [coeff_X_add_one_pow, cast_id]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
choose_eq_zero_of_lt hikl,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Tactic:
choose_eq_zero_of_lt hikl,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ 0 * i.choose l = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
clear! f

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub,
      add_comm x.2 x.1, mul_assoc, ← mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * (r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
← pow_add

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)