mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          (Multiset.map ((fun x ↦ X - C x) ∘ Prod.fst)
              (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots.toEnumFinset.val).prod).coeff
      n =
    0

Tactic:
← Multiset.map_map,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          (Multiset.map (fun x ↦ X - C x)
              (Multiset.map Prod.fst
                (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots.toEnumFinset.val)).prod).coeff
      n =
    0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hx.a.a
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅u, yc⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hu

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (v : ι → R), ∃ n, A ^ n *ᵥ v = 0

Tactic:
simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
    toLin'_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
this : IsNilpotent (LinearMap.restrict (g - (algebraMap R (End R M)) μ) h₂)
⊢ g m = μ • m

Tactic:
by
    replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
    simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case hx
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ x ∈ ⊤.lcs L 1

pp: case hy
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ y ∈ LieSubmodule.ucs 1 ⊥

Tactic:
· simpa using hx

Goal state after:
case hy
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ lowerCentralSeries R L L 1
hy : y ∈ LieAlgebra.center R L
⊢ y ∈ LieSubmodule.ucs 1 ⊥
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case inl
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
x : ↥H
hαx : 0 x = 0
hx : x ∈ corootSpace 0
⊢ x = 0

pp: case inr
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ x = 0

Tactic:
· simpa using hx

Goal state after:
case inr
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ x = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
x : R
⊢ eval (-x) (T R n) = ↑↑n.negOnePow * eval x (T R n)

Tactic:
induction n using Chebyshev.induct' with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)
    · simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]
      ring_nf
    · simp
  | neg n ih => simp [ih]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
hef : ⁅⁅e, f⁆, e⁆ = 2 • e
contra : ⁅e, f⁆ = 0
⊢ False

Tactic:
rw [contra] at hef
    have : IsAddTorsionFree L := .of_isTorsionFree K L
    simp only [zero_lie, eq_comm (a := (0 : L)), smul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hef
    contradiction

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑m ≠ -1
⊢ (U R (-↑m)).degree = ↑((-↑m + 1).natAbs - 1)

Tactic:
U_neg,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑m ≠ -1
⊢ (-U R (↑m - 2)).degree = ↑((-↑m + 1).natAbs - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
h : T R (n + 2) = U R (-(n + 2)) - X * U R (-(n + 2) - 1)
⊢ T R (n + 2) = X * U R (n + 1) - U R n

Tactic:
U_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : T R (n + 2) = -U R (n + 2 - 2) - X * U R (-(n + 2) - 1)
⊢ T R (n + 2) = X * U R (n + 1) - U R n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
h : T R (n + 2) = -U R n - X * U R (-(n + 2 + 1))
⊢ T R (n + 2) = X * U R (n + 1) - U R n

Tactic:
U_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : T R (n + 2) = -U R n - X * -U R (n + 2 + 1 - 2)
⊢ T R (n + 2) = X * U R (n + 1) - U R n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : C R (-(↑n + 1)) = C R (↑n + 1)
ih2 : C R (-↑n) = C R ↑n
⊢ C R (-(↑n + 2)) = C R (↑n + 2)

Tactic:
have h₁ := C_add_two R n

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : C R (-(↑n + 1)) = C R (↑n + 1)
ih2 : C R (-↑n) = C R ↑n
h₁ : C R (↑n + 2) = X * C R (↑n + 1) - C R ↑n
⊢ C R (-(↑n + 2)) = C R (↑n + 2)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
⊢ x ∈ sl2SubmoduleOfRoot hα

Tactic:
obtain ⟨x_αneg, hx_αneg, x_h, ⟨y, hy_coroot, rfl⟩, rfl⟩ := mem_sup.mp hx

Goal state after:
case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
x_αneg : L
hx_αneg : x_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
y : ↥H.toLieSubmodule
hy_coroot : y ∈ ↑↑(corootSpace ⇑α)
hx : x_αneg + ↑H.toLieSubmodule.incl y ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ x_αneg + ↑H.toLieSubmodule.incl y ∈ sl2SubmoduleOfRoot hα
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (-↑n)) = U R' (-↑n)
ih2 : map f (U R (-↑n + 1)) = U R' (-↑n + 1)
⊢ map f (U R (-↑n - 1)) = U R' (-↑n - 1)

Tactic:
simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : NeZero 2
⊢ 0 ∉ range ⇑P.root

Tactic:
simpa only [mem_range, not_exists] using fun i ↦ P.ne_zero i

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace H 0) (U ⊔ V)
⊢ Disjoint U (V ⊔ rootSpace H 0)

Tactic:
convert! key.disjoint_biSup_biSup (hUV.union_right hU0.symm)

Goal state after:
case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace H 0) (U ⊔ V)
⊢ V ⊔ rootSpace H 0 = ⨆ i ∈ sV ∪ s0, LieModule.genWeightSpace L i
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
this : span K (Set.range v') = ⊤
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
let e := (Module.Finite.finite_basis b).equivFin

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
this : span K (Set.range v') = ⊤
e : { x // x ∈ v } ≃ Fin (Nat.card { x // x ∈ v }) := Finite.equivFin { x // x ∈ v }
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case left
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * (algebraMap A K) (↑(den A r) * inv)

Tactic:
← h_inv,

Goal state after:
case left
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * (algebraMap A K) 1
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Order.krullDim (Submodule R M) = 1 ↔ IsSimpleModule R M

Tactic:
Order.krullDim_eq_one_iff_of_boundedOrder,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleModule R M
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
⊢ Nontrivial (R ⧸ comap (algebraMap R S) P)

Tactic:
Quotient.nontrivial_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
⊢ comap (algebraMap R S) P ≠ ⊤
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ p ^ Nat.find ex ∈ I

Tactic:
exact Nat.find_spec ex

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ x ∈ sInf {J | 0 ≤ J ∧ J.IsPrime} ↔ x ∈ IsLocalRing.maximalIdeal R

Tactic:
simp [← Ideal.isMaximal_iff_isPrime, IsLocalRing.isMaximal_iff]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ φ' q'' * (algebraMap (R[X] ⧸ P) Sₘ) (φ q') = φ' q'' * (φ'.comp (algebraMap (R ⧸ P') Rₘ)) ↑⟨q', hq'⟩

Tactic:
simp only [φ', IsLocalization.map_comp _, RingHom.comp_apply]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
⊢ (IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegral

Tactic:
by
  let P' : Ideal R := P.comap C
  let M : Submonoid (R ⧸ P') :=
    Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff
  let M' : Submonoid (R[X] ⧸ P) :=
    (Submonoid.powers (pX.map (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff).map
      (quotientMap P C le_rfl)
  let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C le_rfl
  let φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ M.le_comap_map
  have hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C := rfl
  intro p
  obtain ⟨⟨p', ⟨q, hq⟩⟩, hp⟩ := IsLocalization.surj M' p
  suffices φ'.IsIntegralElem (algebraMap (R[X] ⧸ P) Sₘ p') by
    obtain ⟨q', hq', rfl⟩ := hq
    obtain ⟨q'', hq''⟩ := isUnit_iff_exists_inv'.1 (IsLocalization.map_units Rₘ (⟨q', hq'⟩ : M))
    refine (hp.symm ▸ this).of_mul_unit φ' p (algebraMap (R[X] ⧸ P) Sₘ (φ q')) q'' ?_
    rw [← φ'.map_one, ← congr_arg φ' hq'', φ'.map_mul, ← φ'.comp_apply]
    simp only [φ', IsLocalization.map_comp _, RingHom.comp_apply]
  dsimp at hp
  refine @IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ'
    ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_
    ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_
  · rintro x ⟨p, hp, rfl⟩
    push _ ∈ _ at hp
    rcases hp with hy | hy
    · rw [hy]
      refine φ.isIntegralElem_localization_at_leadingCoeff ((Ideal.Quotient.mk P) X)
        (pX.map (Ideal.Quotient.mk P')) ?_ M ?_
      · rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]
      · use 1
        simp only [P', pow_one]
    · rw [degree_le_zero_iff] at hy
      rw [hy]
      refine ⟨X - C (algebraMap _ _ ((Ideal.Quotient.mk P') (p.coeff 0))), monic_X_sub_C _, ?_⟩
      simp only [eval₂_sub, eval₂_X, eval₂_C]
      rw [sub_eq_zero, ← φ'.comp_apply]
      simp [φ', IsLocalization.map_comp _, P', φ]
  · obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective p'
    rw [← RingHom.comp_apply]
    apply Subring.mem_closure_image_of
    apply Polynomial.mem_closure_X_union_C

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ ¬IsField Aₘ

Tactic:
intro h
  let := h.toField
  obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP
  exact
    (IsLocalRing.maximalIdeal.isMaximal _).ne_top
      (Ideal.eq_top_of_isUnit_mem _
        ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
        (isUnit_iff_ne_zero.mpr
          ((map_ne_zero_iff (algebraMap A Aₘ)
                (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr
            x_ne)))

Goal state after: