mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 0 (T R (-↑n)) = ↑(if Even (-↑n) then ↑(-↑n / 2).negOnePow else 0)
ih2 : eval 0 (T R (-↑n + 1)) = ↑(if Even (-↑n + 1) then ↑((-↑n + 1) / 2).negOnePow else 0)
this : (-↑n + 1) / 2 = (-↑n - 1) / 2 + 1
h✝ : ¬Even n
⊢ eval 0 (T R (-↑n - 1)) = ↑(if Even (-↑n - 1) then ↑((-↑n - 1) / 2).negOnePow else 0)

Tactic:
simp_all [T_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]

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
n : ℤ
⊢ (U R n).natDegree = (n + 1).natAbs - 1

Tactic:
by_cases n = -1
  case pos hn => subst hn; simp
  case neg hn => exact natDegree_eq_of_degree_eq_some (degree_U_of_ne_neg_one R n hn)

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)}
⊢ iSupIndep ![rootSpace H 0, U, V]

Tactic:
have hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i := by simp [hs0]

Goal state after:
ι : 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
⊢ iSupIndep ![rootSpace H 0, U, V]
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have H₂ := T_derivative_eq_U (R := R) (n + 1)

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
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
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ (↑(f.symm ≪≫ₗ P.toPerfPair ≪≫ₗ g.symm.dualMap)).IsPerfPair

Tactic:
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
    have : IsReflexive R N₂ := equiv g
    infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ (range fun n ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y) ⊆ Φ

Tactic:
range_subset_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ ∀ (y_1 : ℕ), (⇑(reflection hgy ≪≫ₗ reflection hfx))^[y_1] y ∈ Φ
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
by
  obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x
  obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
    UniqueFactorizationMonoid.exists_reduced_factors' a b
      (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)
  obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
  refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩
  refine mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_
  simp only [map_mul, Algebra.smul_def] at *
  rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]

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

Goal state before:
pp: case e'_4
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]
r : K
hr : (aeval r) p = 0
⊢ (p.scaleRoots ↑(den A r)).coeff 0 = (p.scaleRoots ↑(den A r)).coeff 0 * num A r ^ 0

Tactic:
rw [pow_zero, mul_one]

Goal state after:
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' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hM : span L ↑i.range = ⊤
hN : span L ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Tactic:
suffices FiniteDimensional K M' from .of_injective (p.restrictScalars_injective_aux i j hi hN hp)
    (p.flip.restrictScalars_injective_aux j i hj hM (fun m n ↦ hp n m))

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' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hM : span L ↑i.range = ⊤
hN : span L ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
⊢ FiniteDimensional K M'
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
f0 : IsMin (f 0)
n : ℕ
hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)
⊢ ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

Tactic:
exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩

Goal state after:
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
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
⊢ RelSeries.last t' = RelSeries.head s'

Tactic:
by simpa [s', t', hs₁, ht₂] using hfg

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.map f (Ideal.span {x, y})

Tactic:
Ideal.map_span,

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {f x, f y} = Ideal.span (⇑f '' {x, y})
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = S ∙ f (gcd x y)

Tactic:
Ideal.map_span,

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span (⇑f '' {gcd x y}) = S ∙ f (gcd x y)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ (MulAction.orbitRel Aˣ K) ((fun m ↦ m • a) b)⁻¹ a⁻¹

Tactic:
use b⁻¹

Goal state after:
case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ (fun m ↦ m • a⁻¹) b⁻¹ = ((fun m ↦ m • a) b)⁻¹
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
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
⊢ Submodule.IsPrincipal I

Tactic:
have ex : ∃ n : ℕ, p ^ n ∈ I := by
    obtain ⟨n, u, rfl⟩ := H hx0
    refine ⟨n, ?_⟩
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hxI

Goal state after:
case neg
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
⊢ Submodule.IsPrincipal I
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I : Ideal R
inst✝ : IsJacobsonRing R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I)

Tactic:
rintro ⟨x⟩
    use x
    rfl

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ Disjoint ↑(powers y) ↑I

Tactic:
disjoint_powers_iff_notMem_of_isPrime

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ y ∉ I
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
⊢ Disjoint ↑(powers y) ↑I

Tactic:
disjoint_powers_iff_notMem_of_isPrime

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
⊢ y ∉ I
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬R ∙ Submodule.IsPrincipal.generator I = ⊥
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Irreducible (Submodule.IsPrincipal.generator I)

Tactic:
Submodule.span_singleton_eq_bot

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ Irreducible (Submodule.IsPrincipal.generator I)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ Disjoint ↑(powers y) ↑I

Tactic:
disjoint_powers_iff_notMem_of_isPrime

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ y ∉ I
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v (x - y) = v y

Tactic:
rw [sub_eq_add_neg, map_add_eq_of_lt_right, map_neg]

Goal state after:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v (-y)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
⊢ (comap C P).IsMaximal

Tactic:
by
  let P' := comap (C : R →+* R[X]) P
  have hP'_prime : P'.IsPrime := comap_isPrime C P
  obtain ⟨⟨m, hmem_P⟩, hm⟩ :=
    Submodule.nonzero_mem_of_bot_lt (bot_lt_of_maximal P (Polynomial.not_isField R))
  have hm' : m ≠ 0 := by
    simpa [Submodule.coe_eq_zero] using hm
  let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P (C : R →+* R[X]) le_rfl
  let a : R ⧸ P' := (m.map (Ideal.Quotient.mk P')).leadingCoeff
  let M : Submonoid (R ⧸ P') := Submonoid.powers a
  rw [← bot_quotient_isMaximal_iff]
  have hp0 : a ≠ 0 := fun hp0' =>
    hm' <| map_injective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))
      ((injective_iff_map_eq_zero (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))).2
        fun x hx => by
          rwa [Quotient.eq_zero_iff_mem, (by rwa [eq_bot_iff] : (P.comap C : Ideal R) = ⊥)] at hx)
        (by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0')
  have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ => hp0 (eq_zero_of_pow_eq_zero hn)
  suffices (⊥ : Ideal (Localization M)).IsMaximal by
    rw [← IsLocalization.under_map_of_isPrime_disjoint M (Localization M) isPrime_bot
      (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]
    exact ((IsLocalization.isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp
      (by rwa [Ideal.map_bot])).1
  let M' : Submonoid (R[X] ⧸ P) := M.map φ
  have hM' : (0 : R[X] ⧸ P) ∉ M' := fun ⟨z, hz⟩ =>
    hM (quotientMap_injective (_root_.trans hz.2 φ.map_zero.symm) ▸ hz.1)
  suffices (⊥ : Ideal (Localization M')).IsMaximal by
    rw [le_antisymm bot_le (comap_bot_le_of_injective _
      (IsLocalization.map_injective_of_injective M (Localization M) (Localization M')
        quotientMap_injective))]
    refine isMaximal_comap_of_isIntegral_of_isMaximal' _ ?_ ⊥
    have isloc : IsLocalization (Submonoid.map φ M) (Localization M') := by infer_instance
    exact @isIntegral_isLocalization_polynomial_quotient R _
      (Localization M) (Localization M') _ _ P m hmem_P _ _ _ isloc
  rw [(map_bot.symm :
    (⊥ : Ideal (Localization M')) = Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)]
  let bot_maximal := (bot_quotient_isMaximal_iff _).mpr hP
  refine bot_maximal.map_bijective (algebraMap (R[X] ⧸ P) (Localization M')) ?_
  apply IsField.localization_map_bijective hM'
  rwa [← Quotient.maximal_ideal_iff_isField_quotient, ← bot_quotient_isMaximal_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap C (comap (Ideal.Quotient.mk P) ⊥)).IsMaximal

Tactic:
comap_comap

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
⊢ Module.Finite R S

Tactic:
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
  have : (algebraMap R S).IsIntegral := by
    rw [← f.comp_algebraMap]
    -- We need to write `f.toRingHom` instead of just `f`, to avoid unification issues.
    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf
  have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this
  exact Algebra.IsIntegral.finite

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
s : ι → R
hs : ∀ i ∈ I, IsSumSq (s i)
⊢ IsSumSq (∑ i ∈ I, s i)

Tactic:
simpa using sum_mem (S := AddSubmonoid.sumSq _) hs

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

Goal state before:
pp: case mem
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ ↑(P.reflection i) (P.root j) ∈ span R (range ⇑P.root)

Tactic:
LinearEquiv.coe_coe,

Goal state after:
case mem
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ (P.reflection i) (P.root j) ∈ span R (range ⇑P.root)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ span R (range (⇑↑P.toPerfPair ∘ ⇑P.root)) = span R (range P.root')

Tactic:
LinearEquiv.coe_coe,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ span R (range (⇑P.toPerfPair ∘ ⇑P.root)) = span R (range P.root')
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
s : S
⊢ (algebraMap S R) s = (B.form ↑x) ↑y ↔ s = (B.posForm x) y

Tactic:
simp [RootPositiveForm.posForm]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
h : P.pairingIn S i j ≤ 0
⊢ P.pairingIn S j i ≤ 0

Tactic:
← not_lt,

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
h : P.pairingIn S i j ≤ 0
⊢ ¬0 < P.pairingIn S j i
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
⊢ h.orderMonoidIso (v.restrict a) = w.restrict a

Tactic:
by
  have h_res := h.restrict
  by_cases ha : v a = 0
  · rw [← restrict_eq_zero_iff] at ha
    rwa [ha, map_zero, Eq.comm, ← h_res.eq_zero]
  · rw [(v.restrict_eq_mk ha)]
    simp [orderMonoidIso, valueGroup₀Fun_spec h (hs := ha),
      w.restrict_eq_mk ((eq_zero h.symm).ne.mpr ha)]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ v x ≤ v y ↔ v' x ≤ v' y

Tactic:
← div_le_one₀,

Goal state after:
case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ v x / v y ≤ 1 ↔ v' x ≤ v' y

case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ 0 < v y