mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = 1 i j

Tactic:
rw [one_eq_pi_single, Pi.single_comm, ← hcols j]

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = (A *ᵥ cols j) i
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C

Tactic:
← inv_eq_right_inv h,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ A⁻¹ = C
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C

Tactic:
← inv_eq_right_inv h,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ A⁻¹ = C
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * M *
      (List.map toMatrix ({ i := inl i, j := inr (), hij := ⋯, c := 1 } :: L')).prod).IsTwoBlockDiagonal

Tactic:
simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, List.map]

Goal state after:
case pos.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * M * transvection (inl i) (inr ()) 1 * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) (p %ₘ f) + (aeval x) f * (aeval x) (p /ₘ f) ∈
    span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
hfx,

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) (p %ₘ f) + 0 * (aeval x) (p /ₘ f) ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
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
⊢ map f I ≤ Submodule.span T (⇑f '' generators I)

Tactic:
refine map_le_of_le_comap (fun r hr ↦ ?_)

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
r : R
hr : r ∈ I
⊢ r ∈ comap f (Submodule.span T (⇑f '' generators I))
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
⊢ (1 + X • M.map ⇑C).det = 1 + (C ((1 + X • M.map ⇑C).det.divX.coeff 0) + (1 + X • M.map ⇑C).det.divX.divX * X) * X

Tactic:
add_comm (C _),

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + ((1 + X • M.map ⇑C).det.divX.divX * X + C ((1 + X • M.map ⇑C).det.divX.coeff 0)) * X
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a + b)! / (↑a ! * ↑(a + b - a)!) = ↑(a + b)! / (↑a ! * ↑b !)

Tactic:
Nat.add_sub_cancel_left

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a + b)! / (↑a ! * ↑b !) = ↑(a + b)! / (↑a ! * ↑b !)
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' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
⊢ Function.Injective ⇑f.toLinearMap

Tactic:
← LinearMap.ker_eq_bot,

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 :=
  { 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' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
⊢ f.toLinearMap.ker = ⊥
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ r • x ∈ S[x]

Tactic:
by
    rw [← algebraMap_smul S]; apply Subalgebra.smul_mem; exact Algebra.subset_adjoin rfl

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

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

Tactic:
· rw [← tsub_lt_iff_right hil] at hikl
      rw [choose_eq_zero_of_lt hikl, zero_mul]

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

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

Tactic:
hasseDeriv_one

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ eval r (derivative f) = eval r (derivative f)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).coeff p.natDegree = p.coeff p.natDegree

Tactic:
coeff_scaleRoots,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ p.coeff p.natDegree * s ^ (p.natDegree - p.natDegree) = p.coeff p.natDegree
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : p.degree = ↑i
⊢ 1 * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
· simp [natDegree_eq_of_degree_eq_some h, leadingCoeff]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).scaleRoots r * p.scaleRoots r = p.scaleRoots r ^ (n + 1)

pp: case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
IH,

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.scaleRoots r ^ n * p.scaleRoots r = p.scaleRoots r ^ (n + 1)

case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-f).Splits

Tactic:
rw [← neg_one_mul, ← C_1, ← C_neg]

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (C (-1) * f).Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : (aeval ((integralClosure R A).val x)) p = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0

Tactic:
aeval_algHom_apply

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : (integralClosure R A).val ((aeval x) p) = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case mk
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ (Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk (⇑(quotientRel I)) x)

Tactic:
refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩

Goal state after:
case mk
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I)) x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg.a
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n ∈ (algebraMap R Rₘ).range

Tactic:
rw [← Algebra.smul_def]
      exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ f.Splits

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.mpr h₂, splits_mul (X_sub_C_ne_zero x) (by aesop)]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ (X - C x).Splits ∧ (f /ₘ (X - C x)).Splits
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ Function.Injective
    ⇑(quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)

Tactic:
refine quotientMap_injective' (le_of_eq ?_)

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) (map (mapRingHom (Quotient.mk (comap C P))) P) = P
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this : IsIntegral R (⟨r, hr⟩ ^ m • x)
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
exact ⟨m, this⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
⊢ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤

Tactic:
cases x
  rfl

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
⊢ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal

Tactic:
cases x
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ φ.toRingHom t q * t ^ N = 0

Tactic:
hqt,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ 0 * t ^ N = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a * b)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a + b)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p ∈ I.minimalPrimes, y ∉ p

Tactic:
simpa [← Ideal.sInf_minimalPrimes] using hy

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S ↥(ofField K S hS)

Tactic:
ofField_eq

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S ↥(subalgebra K S hS)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
⊢ ∀ (a b c : α), le a c → le b c → le (sup a b) c

Tactic:
intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_sup, hac, hbc]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ False

Tactic:
have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
⊢ False
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ i, a ∈ u i

Tactic:
by
  simpa [← hu.iSup_set_eq_univ] using mem_univ a

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ ↑U = ∅ ∨ ↑U = univ

Tactic:
← IndiscreteTopology.isOpen_iff

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ IsOpen[inst✝¹] ↑U
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : ↑s
⊢ IsCompact (s.restrictPreimage f ⁻¹' {y})

Tactic:
rw [IsEmbedding.subtypeVal.isCompact_iff, image_val_preimage_restrictPreimage, image_singleton]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : ↑s
⊢ IsCompact (f ⁻¹' {↑y})
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ b ⊔ aᶜ ∈ L

Tactic:
exact L.supClosed hb (compl_mem ha)

Goal state after:
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ QuasiSeparatedSpace α

Tactic:
quasiSeparatedSpace_iff

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔
    ∀ (U V : Set α), IsOpen[inst✝] U → IsCompact U → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
x : X
hx : x ∈ K
V : Set X
h : V ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}
hxV : x ∈ V
hVU : V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
exact ⟨V, mem_nhdsWithin.mpr ⟨V, h.1, hxV, Set.inter_subset_left⟩, V, h.2, h.1, subset_rfl, hVU⟩

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ ((Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d)) x = (IsScalarTower.toAlgHom R A (B ⧸ I)) x

Tactic:
exact liftOfDerivationToSquareZero_mk_apply I hI d x

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
Q : Ideal R
inst✝ : Q.IsPrime
hQP : Q = Ideal.comap f P
⊢ (Localization.localRingHom Q P f hQP).Flat

Tactic:
subst hQP

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMLeft b ≠ 0

Tactic:
rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]

Goal state after:
a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ CompactSpace (PrimeSpectrum R)

Tactic:
by
  refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
  choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
  simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
  exact CompleteLattice.IsCompactElement.exists_finset_of_le_iSup _
    Ideal.isCompactElement_top _ S_empty

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosed (Set.range (comap (RingHom.snd R S)))

Tactic:
simp_rw [range_comap_snd, isClosed_zeroLocus]

Goal state after: