mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ 2 • ⇑(P.reflection i) = 2 • ⇑(P.reflection j)

Tactic:
ext x
  suffices
      2 • P.toLinearMap x (P.coroot i) • P.root i = 2 • P.toLinearMap x (P.coroot j) • P.root j by
    simpa [reflection_apply, smul_sub]
  calc 2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_
  · rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
  · rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]
  · rw [← smul_comm, ← smul_assoc, map_smul]
  · rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]
  · rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]

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

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

Tactic:
Function.comp_apply

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

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

Tactic:
Function.comp_apply

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (0 + 0) * T R (n + 1) + (↑n + 1) * (↑(n + 1) * U R (n + 1 - 1)) =
    1 * U R n + X * derivative (U R n) -
      ((0 - ↑2 * X ^ (2 - 1)) * derivative (U R n) + (1 - X ^ 2) * derivative (derivative (U R n)))
⊢ (1 - X ^ 2) * derivative (derivative (U R n)) = 3 * X * derivative (U R n) - (↑n + 2) * ↑n * U R n
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 χ
⊢ iSupIndep ![rootSpace H 0, U, V]

Tactic:
have h₀ : Disjoint (rootSpace H 0) (U ⊔ V) := by
    convert! key.disjoint_biSup_biSup (hU0.union_right hV0)
    rw [iSup_union, hsU', hsV']

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
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)
⊢ iSupIndep ![rootSpace H 0, U, V]
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ IsInteger A x

Tactic:
use ↑d⁻¹ * num A x

Goal state after:
case h
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ (algebraMap A K) (↑d⁻¹ * num A x) = x
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ comap (factor hJK) (map (mk J) I)
⊢ x ∈ map (mk K) I

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk J) Quotient.mk_surjective h with ⟨r, hr, eq⟩
    have : x - ((mk K) r) ∈ J.map (mk K) := by
      simp [← factor_ker hJK, ← eq]
    rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective this with ⟨s, hs, eq'⟩
    rw [← add_sub_cancel ((mk K) r) x, ← eq', ← map_add]
    exact mem_map_of_mem (mk K) (Submodule.add_mem _ hr (hIJ hs))

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b : WithZero αˣ
⊢ a < b → withZeroUnitsEquiv a < withZeroUnitsEquiv b

Tactic:
cases a <;> cases b

Goal state after:
case zero.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ 0 < 0 → withZeroUnitsEquiv 0 < withZeroUnitsEquiv 0

case zero.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ 0 < ↑a✝ → withZeroUnitsEquiv 0 < withZeroUnitsEquiv ↑a✝

case coe.zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝ : αˣ
⊢ ↑a✝ < 0 → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv 0

case coe.coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a✝¹ a✝ : αˣ
⊢ ↑a✝¹ < ↑a✝ → withZeroUnitsEquiv ↑a✝¹ < withZeroUnitsEquiv ↑a✝
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
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
⊢ length R M = length R N + length R P

Tactic:
have := mt (IsFiniteLength.of_injective · hf) hN
      rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
      rw [hN, this, top_add]

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

Goal state before:
pp: case mpr.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ v ((algebraMap O F) x) ∈ upperBounds (⇑v ∘ ⇑(algebraMap O F) '' ↑I)

Tactic:
simp [hx, mem_upperBounds]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring

Goal state after:
case inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
this : x * a + y * b = 1
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
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
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hxy : x * y ∈ (Ideal.comap (algebraMap R S) P').jacobson
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
rw [hP] at hxy

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
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hxy : x * y ∈ under R P'
⊢ x ∈ Ideal.comap (algebraMap R S) P'
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v

Tactic:
apply (hirr.ne_zero (eq_zero_of_pow_eq_zero h)).elim

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : IsField R
⊢ ∃ n, I = maximalIdeal R ^ n

pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
· let _ := h.toField
    exact ⟨0, by simp [(eq_bot_or_eq_top I).resolve_left hI]⟩

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
⊢ ∃ n, I = maximalIdeal R ^ n
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
⊢ x ∈ S i

Tactic:
algebraize [(Subalgebra.inclusion le).toRingHom]

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
⊢ x ∈ S i
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀✝
v✝ : Valuation R Γ₀✝
Γ₀ : Type u_7
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
⊢ Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueMonoid

Tactic:
by
  obtain ⟨x, h0, h1⟩ := hv.exists_val_nontrivial
  rw [Submonoid.nontrivial_iff_exists_ne_one]
  use (Units.mk0 (v x) h0), (MonoidWithZeroHom.ofClass v).mem_valueMonoid (Set.mem_range_self x)
  simpa [Units.ext_iff]

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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
by
  obtain ⟨x, hx⟩ := isNontrivial_iff_exists_unit.mp hv
  rw [ne_iff_lt_or_gt] at hx
  rcases hx with hx | hx
  · use x
    simp [hx]
  · use x⁻¹
    simp [-map_inv₀, ← one_lt_val_iff, hx]

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
⊢ Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤

Tactic:
contrapose! hx with h

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
⊢ ∀ y ∈ M, x * y ∈ M
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective ⇑φ := quotientMap_injective
Rₘ : Type u_5 := Localization.Away x
⊢ ⊥.jacobson = ⊥

Tactic:
let Sₘ := (Localization ((Submonoid.powers x).map φ : Submonoid (R[X] ⧸ P)))

Goal state after:
case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective ⇑φ := quotientMap_injective
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
⊢ ⊥.jacobson = ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case hg
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ w.toRingEquiv.toRingHom.IsIntegral

Tactic:
apply RingHom.isIntegral_of_surjective

Goal state after:
case hg
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ Function.Surjective ⇑w.toRingEquiv.toRingHom
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin 0) R ⧸ P)).IsIntegral

Tactic:
apply RingHom.isIntegral_of_surjective

Goal state after:
case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
⊢ (f.comp C).IsIntegral

Tactic:
have e := (Fintype.equivFin σ).symm

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
⊢ (f.comp C).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
⊢ (f'.comp C).IsIntegral

Tactic:
let g : MvPolynomial _ R ⧸ (RingHom.ker f') →+* S :=
      Ideal.Quotient.lift (RingHom.ker f') f' fun _ h => h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
⊢ (f'.comp C).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

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
B : P.InvariantForm
i j : ι
⊢ 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)

Tactic:
two_mul,

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
B : P.InvariantForm
i j : ι
⊢ (B.form (P.root i)) (P.root j) + (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)
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
i : ι
hi : P.root i ∈ span S (range ⇑P.root)
⊢ 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root i, hi⟩

Tactic:
by
  simpa only [zero_lt_posForm_iff] using B.exists_pos_eq i

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    (P.PolarizationIn S) (P.rootSpanMem S i) + (P.PolarizationIn S) (P.rootSpanMem S i)

Tactic:
nth_rw 2 [hP]

Goal state after:
ι : 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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    (P.PolarizationIn S) (P.rootSpanMem S i) +
      ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)