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 : ι
⊢ P.toPerfPair.conj ↑(P.reflection i) = (↑(P.coreflection i)).dualMap

Tactic:
by
  ext f n
  simp [reflection_apply, coreflection_apply, mul_comm (f <| P.coroot i)]

Goal state after:
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)
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))

Tactic:
have h₁ := T_add_two R n

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)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    T_derivative_eq_U, C_eq_natCast] at h₁

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

Goal state before:
pp: case mem
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
i : ι
his : i ∈ s
⊢ (P.reflection j) (P.root i) = P.root i

Tactic:
exact IsOrthogonal.reflection_apply_right <| hj i his

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
⊢ 2 * g x = 4

Tactic:
hgx

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
⊢ 2 * 2 = 4
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
⊢ Injective ⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp)

Tactic:
← LinearMap.ker_eq_bot

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).ker = ⊥
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 y : K
h : num A y * ↑(den A x) = num A x * ↑(den A y)
⊢ x = y

Tactic:
simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h

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

Goal state before:
pp: case e
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ (aeval ((algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s) x✝

Tactic:
rw [aeval_def, mk'_spec' _ r s]

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

Goal state before:
pp: case neg_add_one
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)
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)

Tactic:
have h₁ := T_mul_T R ((-m) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ Function.Injective ⇑(powSMulQuotInclusion I M h N)

Tactic:
← LinearMap.ker_eq_bot

Goal state after:
R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
N : Submodule R M
⊢ (powSMulQuotInclusion I M h N).ker = ⊥
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
⊢ 0 < length R M ↔ Nontrivial M

Tactic:
rw [pos_iff_ne_zero, ne_eq, Module.length_eq_zero_iff, not_subsingleton_iff_nontrivial]

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
⊢ FiniteDimensionalOrder (Submodule R M) ↔ IsFiniteLength R M

Tactic:
rw [← Module.length_ne_top_iff_finiteDimensionalOrder, Module.length_ne_top_iff]

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
⊢ FiniteDimensionalOrder (Submodule R M) ↔ IsFiniteLength R M

Tactic:
by
  rw [← Module.length_ne_top_iff_finiteDimensionalOrder, Module.length_ne_top_iff]

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 : S
⊢ Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y

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
⊢ Submodule.IsPrincipal (Ideal.span {f x, f y})
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b : ValueGroup A K
a : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ b ∨ b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a

Tactic:
rcases b with ⟨b⟩

Goal state after:
case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
a b : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ v 1 ≤ v ((algebraMap O R) x)

Tactic:
← (algebraMap O R).map_one,

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ v ((algebraMap O R) 1) ≤ v ((algebraMap O R) 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 : v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)
⊢ b ∈ I

Tactic:
· rw [le_iff_dvd hv] at h
      exact Ideal.mem_of_dvd I h ha

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

Goal state before:
pp: case pos
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
h : ∀ x ∈ α, x ∈ β
⊢ α ≤ β ∨ β ≤ α

Tactic:
exact Or.inl h

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
⊢ Function.Injective ⇑(of I M)

Tactic:
← LinearMap.ker_eq_bot

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
⊢ (of I M).ker = ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case mp
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 : J.IsPrime
⊢ (under R J).IsMaximal

Tactic:
isPrime_iff_isPrime_disjoint (Submonoid.powers y)

Goal state after:
case mp
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)
⊢ (under R J).IsMaximal
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ span {generator s} = span {ϖ ^ n}

Tactic:
← hnu,

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
gen_ne_zero : generator s ≠ 0
n : ℕ
u : Rˣ
hnu : generator s * ↑u = ϖ ^ n
this : span {generator s} = s
⊢ span {generator s} = span {generator s * ↑u}
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
⊢ ∀ {p : Ideal Rₘ}, p ≠ ⊥ → p.IsPrime → p.IsMaximal

Tactic:
intro p hp0 hpp
  refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
  have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
  rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
  refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩
  exact IsLocalization.bot_lt_under_prime _ _ hM _ hp0

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_2
inst✝¹ : _root_.Finite ι
inst✝ : IsJacobsonRing R
⊢ IsJacobsonRing (MvPolynomial ι R)

Tactic:
cases nonempty_fintype ι
  let e := Fintype.equivFin ι
  rw [isJacobsonRing_iso (renameEquiv R e).toRingEquiv]
  exact isJacobsonRing_MvPolynomial_fin _

Goal state after:
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:
by
  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✝¹ : AddZeroClass R
inst✝ : Mul R
a : R
⊢ IsSumSq (a * a)

Tactic:
simpa using sq_add a zero

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

Goal state before:
pp: case hB
ι : 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
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
i j : ι
⊢ ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) (P.root i)) (P.root j) ∈ (Algebra.linearMap S R).range

Tactic:
simpa using B.exists_eq i j

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

Goal state before:
pp: ι : 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)
⊢ 2 • P.Polarization (P.root k) = 2 • P.Polarization (m • P.root i) + 2 • P.Polarization (n • P.root j)

Tactic:
← nsmul_add,

Goal state after:
ι : 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)
⊢ 2 • P.Polarization (P.root k) = 2 • (P.Polarization (m • P.root i) + P.Polarization (n • P.root j))
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x = 1 ↔ v' x = 1) → v.IsEquiv v'

Tactic:
· intro h
    apply isEquiv_of_val_le_one
    intro x
    constructor
    · intro hx
      rcases lt_or_eq_of_le hx with hx' | hx'
      · have : v (1 + x) = 1 := by
          rw [← v.map_one]
          apply map_add_eq_of_lt_left
          simpa
        rw [h] at this
        rw [show x = -1 + (1 + x) by simp]
        refine le_trans (v'.map_add _ _) ?_
        simp [this]
      · rw [h] at hx'
        exact le_of_eq hx'
    · intro hx
      rcases lt_or_eq_of_le hx with hx' | hx'
      · have : v' (1 + x) = 1 := by
          rw [← v'.map_one]
          apply map_add_eq_of_lt_left
          simpa
        rw [← h] at this
        rw [show x = -1 + (1 + x) by simp]
        refine le_trans (v.map_add _ _) ?_
        simp [this]
      · rw [← h] at hx'
        exact le_of_eq hx'

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

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 : ι
inst✝ : P.IsReduced
h : i ≠ j
h' : P.root i ≠ -P.root j
⊢ LinearIndependent R ![P.root i, P.root j]

Tactic:
have := IsReduced.eq_or_eq_neg (P := P) i j
  simp_all

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 ι
i j : ι
⊢ 4 • (P.RootForm (P.root i)) (P.root j) ^ 2 =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
have hij : 4 • (P.RootForm (P.root i)) (P.root j) =
      2 • P.toLinearMap (P.root j) (2 • P.Polarization (P.root i)) := by
    rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
  have hji : 2 • (P.RootForm (P.root i)) (P.root j) =
      P.toLinearMap (P.root i) (2 • P.Polarization (P.root j)) := by
    rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]
  rw [sq, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul, hij, ← rootForm_self_smul_coroot,
    smul_mul_assoc 2, ← mul_smul_comm, hji, ← rootForm_self_smul_coroot, map_smul, ← pairing,
    map_smul, ← pairing, smul_eq_mul, smul_eq_mul, smul_eq_mul, coxeterWeight]
  ring

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : y ∈ p j
⊢ x + t • y ∈ ∅

Tactic:
contradiction

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

Goal state before:
pp: case a
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
hα : ¬α.IsZero
e : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H ((-(↑(chainBotCoeff (⇑α) β).succ + ↑(chainTopCoeff (⇑α) β)) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥

Tactic:
neg_add,

Goal state after:
case a
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
hα : ¬α.IsZero
e : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H ((-↑(chainBotCoeff (⇑α) β).succ + -↑(chainTopCoeff (⇑α) β) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H ((-(↑n + ↑(chainTopCoeff (⇑α) β)) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥

Tactic:
neg_add,

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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α) β
this : rootSpace H ((-↑n + -↑(chainTopCoeff (⇑α) β) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
⊢ rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∑ i ∈ s with 0 < c i, c i • v i + ∑ x ∈ s with 0 < -c x, c x • v x = ∑ i ∈ s, c i • v i

Tactic:
← Finset.sum_union,

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∑ x ∈ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i}, c x • v x = ∑ i ∈ s, c i • v i

ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})