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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (↑k + 1) = C R (m + (↑k + 1)) + C R (m - (↑k + 1))
ih2 : C R m * C R ↑k = C R (m + ↑k) + C R (m - ↑k)
h₁ : C R (m + ↑k + 2) = X * C R (m + ↑k + 1) - C R (m + ↑k)
h₂ : C R (m - ↑k - 2) = X * C R (m - ↑k - 1) - C R (m - ↑k)
h₃ : C R (↑k + 2) = X * C R (↑k + 1) - C R ↑k
⊢ C R m * C R (↑k + 2) +
        (C R m * (X * C R (↑k + 1) - C R ↑k) + C R (m - ↑k - 2) + C R (m + ↑k + 2) + C R m * C R ↑k +
          X * (C R (m + (↑k + 1)) + C R (m - (↑k + 1)))) -
      (C R (m + (↑k + 2)) + C R (m - (↑k + 2)) +
        (C R m * C R (↑k + 2) + (X * C R (m - ↑k - 1) - C R (m - ↑k)) + (X * C R (m + ↑k + 1) - C R (m + ↑k)) +
            (C R (m + ↑k) + C R (m - ↑k)) +
          X * (C R m * C R (↑k + 1)))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
h₁ : C R (m + (-↑k - 1) + 2) = X * C R (m + (-↑k - 1) + 1) - C R (m + (-↑k - 1))
h₂ : C R (m - (-↑k - 1) - 2) = X * C R (m - (-↑k - 1) - 1) - C R (m - (-↑k - 1))
h₃ : C R (-↑k - 1 + 2) = X * C R (-↑k - 1 + 1) - C R (-↑k - 1)
⊢ C R m * C R (-↑k - 1) +
        (C R m * (X * C R (-↑k - 1 + 1) - C R (-↑k - 1)) + C R (m - (-↑k - 1) - 2) + C R (m + (-↑k - 1) + 2) +
            C R m * C R (-↑k + 1) +
          X * (C R (m + -↑k) + C R (m - -↑k))) -
      (C R (m + (-↑k - 1)) + C R (m - (-↑k - 1)) +
        (C R m * C R (-↑k - 1 + 2) + (X * C R (m - (-↑k - 1) - 1) - C R (m - (-↑k - 1))) +
              (X * C R (m + (-↑k - 1) + 1) - C R (m + (-↑k - 1))) +
            (C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))) +
          X * (C R m * C R (-↑k)))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
h₂ : (T R (↑m + 2)).comp (T R n) = ↑2 * T R n * (T R (↑m + 1)).comp (T R n) - (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) +
        (T R (↑m * n) + (T R (↑m + 2)).comp (T R n) + 2 * T R ((↑m + 1) * n) * T R n +
          2 * T R n * (T R (↑m + 1)).comp (T R n)) -
      ((T R (↑m + 2)).comp (T R n) +
        ((T R ↑m).comp (T R n) + (↑2 * T R n * (T R (↑m + 1)).comp (T R n) - (T R ↑m).comp (T R n)) +
            (T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)) +
          2 * T R n * T R ((↑m + 1) * n))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
h₁ : 2 * T R (-↑m * n) * T R n = T R (-↑m * n + n) + T R (-↑m * n - n)
h₂ : (T R (-↑m - 1 + 2)).comp (T R n) = ↑2 * T R n * (T R (-↑m - 1 + 1)).comp (T R n) - (T R (-↑m - 1)).comp (T R n)
⊢ T R ((-↑m - 1) * n) +
        (T R ((-↑m + 1) * n) + (T R (-↑m - 1 + 2)).comp (T R n) + 2 * T R (-↑m * n) * T R n +
          2 * T R n * (T R (-↑m)).comp (T R n)) -
      ((T R (-↑m - 1)).comp (T R n) +
        ((T R (-↑m + 1)).comp (T R n) + (↑2 * T R n * (T R (-↑m - 1 + 1)).comp (T R n) - (T R (-↑m - 1)).comp (T R n)) +
            (T R (-↑m * n + n) + T R (-↑m * n - n)) +
          2 * T R n * T R (-↑m * n))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : C R ((↑m + 1) * n) = (C R (↑m + 1)).comp (C R n)
ih2 : C R (↑m * n) = (C R ↑m).comp (C R n)
h₁ : C R ((↑m + 1) * n) * C R n = C R ((↑m + 1) * n + n) + C R ((↑m + 1) * n - n)
h₂ : (C R (↑m + 2)).comp (C R n) = C R n * (C R (↑m + 1)).comp (C R n) - (C R ↑m).comp (C R n)
⊢ C R ((↑m + 2) * n) +
        (C R (↑m * n) + (C R (↑m + 2)).comp (C R n) + C R ((↑m + 1) * n) * C R n +
          C R n * (C R (↑m + 1)).comp (C R n)) -
      ((C R (↑m + 2)).comp (C R n) +
        ((C R ↑m).comp (C R n) + (C R n * (C R (↑m + 1)).comp (C R n) - (C R ↑m).comp (C R n)) +
            (C R ((↑m + 1) * n + n) + C R ((↑m + 1) * n - n)) +
          C R n * C R ((↑m + 1) * n))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : C R (-↑m * n) = (C R (-↑m)).comp (C R n)
ih2 : C R ((-↑m + 1) * n) = (C R (-↑m + 1)).comp (C R n)
h₁ : C R (-↑m * n) * C R n = C R (-↑m * n + n) + C R (-↑m * n - n)
h₂ : (C R (-↑m - 1 + 2)).comp (C R n) = C R n * (C R (-↑m - 1 + 1)).comp (C R n) - (C R (-↑m - 1)).comp (C R n)
⊢ C R ((-↑m - 1) * n) +
        (C R ((-↑m + 1) * n) + (C R (-↑m - 1 + 2)).comp (C R n) + C R (-↑m * n) * C R n +
          C R n * (C R (-↑m)).comp (C R n)) -
      ((C R (-↑m - 1)).comp (C R n) +
        ((C R (-↑m + 1)).comp (C R n) + (C R n * (C R (-↑m - 1 + 1)).comp (C R n) - (C R (-↑m - 1)).comp (C R n)) +
            (C R (-↑m * n + n) + C R (-↑m * n - n)) +
          C R n * C R (-↑m * n))) =
    0

Tactic:
ring_nf

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f (-x) = f x

Tactic:
← neg_one_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f (-1 * x) = f x
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
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
H : ¬length R R = ⊤
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

Tactic:
rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at H

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
H : IsNoetherian R R ∧ IsArtinian R R
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R
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
c : 0 = 1
⊢ False

Tactic:
obtain ⟨d, hd⟩ := Quotient.exact' c
    apply_fun fun t => d⁻¹ • t at hd
    dsimp at hd
    simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd

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

Goal state before:
pp: 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
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x

Tactic:
refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩

Goal state after:
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
x y : O
⊢ DvdNotUnit x y → x ∣ y ∧ ¬y ∣ x
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.mpr
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
h : a ∣ b
⊢ b ∈ I

Tactic:
exact Ideal.mem_of_dvd I h ha

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : R
⊢ r ∈ I ^ n → ∀ (n_1 : AdicCompletion I M), r • ↑n_1 n = 0

Tactic:
r_in

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : R
r_in : r ∈ I ^ n
⊢ ∀ (n_1 : AdicCompletion I M), r • ↑n_1 n = 0
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
⊢ Submodule.factorPow I N ⋯ ∘ₗ f n = f m

Tactic:
by
  ext x
  symm
  refine Submodule.eq_factor_of_eq_factor_succ ?_ (fun n ↦ f n x) ?_ hle
  · exact fun _ _ le ↦ smul_mono_left (Ideal.pow_le_pow_right (ha.monotone le))
  · intro s
    simp only [LinearMap.ext_iff] at hf
    simpa using (hf x).symm

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

Goal state before:
pp: case refine_3
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)
⊢ R ∙ Submodule.IsPrincipal.generator I = span {p}

Tactic:
apply span_singleton_eq_span_singleton.mpr

Goal state after:
case refine_3
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)
⊢ Associated (Submodule.IsPrincipal.generator I) p
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -x * y) * L - 1 = 0

Tactic:
neg_mul

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -(x * y)) * L - 1 = 0
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
⊢ IsJacobsonRing S

Tactic:
by
  rw [isJacobsonRing_iff_prime_eq]
  refine fun P' hP' => le_antisymm ?_ le_jacobson
  obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'
  have hP := H.out hP'.isRadical
  refine (IsLocalization.map_under (powers y) S P'.jacobson).ge.trans
    ((map_mono ?_).trans (IsLocalization.map_under (powers y) S P').le)
  have : sInf { I : Ideal R | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I } ≤
      comap (algebraMap R S) P' := by
    intro x hx
    have hxy : x * y ∈ (comap (algebraMap R S) P').jacobson := by
      rw [Ideal.jacobson, Ideal.mem_sInf]
      intro J hJ
      by_cases h : y ∈ J
      · exact J.mul_mem_left x h
      · exact J.mul_mem_right y ((mem_sInf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩)
    rw [hP] at hxy
    rcases hP'.mem_or_mem hxy with hxy | hxy
    · exact hxy
    · exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim
  refine le_trans ?_ this
  rw [Ideal.jacobson, under_def, comap_sInf', sInf_eq_iInf]
  refine iInf_le_iInf_of_subset fun I ⟨hI, hIm, hyI⟩ => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩
  · exact ⟨le_trans (IsLocalization.map_under (powers y) S P').symm.le (map_mono hI),
      isMaximal_of_isMaximal_disjoint y I hIm hyI⟩
  · exact IsLocalization.under_map_of_isPrime_disjoint _ S hIm.isPrime <|
      (disjoint_powers_iff_notMem_of_isPrime y).2 hyI

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

pp: case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
· intro p1 p2 h1 h2
    exact Subring.add_mem _ h1 h2

Goal state after:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : ⊤ = (addVal R) y
hx : x = 0
⊢ Associated 0 y

Tactic:
rw [addVal_eq_top_iff.mp h.symm]

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

Goal state before:
pp: case neg
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✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
H : ¬(v x ≠ 0 ∨ v y ≠ 0)
⊢ (↑(restrict₀ (ofClass v))).toFun (x + y) ≤
    max ((↑(restrict₀ (ofClass v))).toFun x) ((↑(restrict₀ (ofClass v))).toFun y)

Tactic:
simp only [ne_eq, not_or, Decidable.not_not] at H
      simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply,
        MonoidWithZeroHom.coe_ofClass, H, ↓reduceDIte, max_self, nonpos_iff_eq_zero]
      replace H : v (x + y) = 0 :=
        le_antisymm (map_add_le _ (le_of_eq H.1) (le_of_eq H.2)) zero_le
      simp [H]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
⊢ v.IsEquiv v' ↔ ∀ {x y : R}, v x < v y ↔ v' x < v' y

Tactic:
by
  simp only [IsEquiv, le_iff_le_iff_lt_iff_lt]
  exact forall_comm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
tfae_have 1 → 4
  | H => ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
rw [← hfg, RingHom.coe_comp] at hf

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g
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
i : ι
x : M
hx : x ∈ span R (range ⇑P.root)
⊢ x ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'

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
inst✝ : Fintype ι
m : M
h : P.flip.toPerfPair (P.Polarization m) = 0
⊢ P.Polarization m = 0

Tactic:
simpa only [EmbeddingLike.map_eq_zero_iff] using h

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
inst✝ : Fintype ι
m : M
⊢ P.Polarization m = 0 ↔ P.RootForm m = 0

Tactic:
rw [← flip_comp_polarization_eq_rootForm]
  refine ⟨fun h ↦ by simp [h], ?_⟩
  rintro (h : P.flip.toPerfPair (P.Polarization m) = 0)
  simpa only [EmbeddingLike.map_eq_zero_iff] using h

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

Goal state before:
pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (P.pairing j i * (m * m * lsq i)) • P.coroot k + (P.pairing j i * (m * n * (P.pairing i j * lsq j))) • P.coroot k +
      (P.pairing j i * (n * n * lsq j)) • P.coroot k =
    (P.pairing j i * (m * lsq i)) • P.coroot i + (P.pairing j i * (n * lsq j)) • P.coroot j
⊢ (m * (P.pairing j i * lsq i)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j =
    (P.pairing j i * (m * lsq i)) • P.coroot i + (P.pairing j i * (n * lsq j)) • P.coroot j

Tactic:
ring_nf

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ chainLength α β • x = ⁅coroot α, x⁆

Tactic:
chainLength_nsmul _ _ hx

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ ⁅coroot α, x⁆ = ⁅coroot α, x⁆
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Tactic:
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
  constructor
  · rintro ⟨⟨hle₁, hle₂⟩, ha⟩
    obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
    exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
  · rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
    refine ⟨⟨hle₁, hle₂⟩, ?_⟩
    rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
    rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
    rwa [Prod.mk_eq_zero]

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

Goal state before:
pp: case h₂
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : ↑(↑(chainLength α 0) - 2 * ↑(chainTopCoeff (⇑α) 0)) = 0 (coroot α)
⊢ chainTopCoeff (⇑α) 0 + 1 + 1 ≤ chainLength α 0

Tactic:
simp only [← @Nat.cast_two ℤ, ← Nat.cast_mul, zero_apply, Int.cast_eq_zero, sub_eq_zero,
    Nat.cast_inj] at this

Goal state after:
case h₂
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : chainLength α 0 = 2 * chainTopCoeff (⇑α) 0
⊢ chainTopCoeff (⇑α) 0 + 1 + 1 ≤ chainLength α 0
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
⊢ span K (⇑P.root '' ({i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q})) = ⊤

Tactic:
have : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = Set.univ := by ext; simp [em]

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
this : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = univ
⊢ span K (⇑P.root '' ({i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q})) = ⊤