mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ lowerCentralSeries R L L 1
⊢ x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}

Tactic:
rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L L 0, ⁅x_1, n⁆ = x}
⊢ x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'

Tactic:
← sub_eq_zero,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ - ((killingForm K L) e) f • ↑α' = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst✝ : LieModule.IsTrivial ↥I ↥N
hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := ⋯
n : ↥N
⊢ ↑(((φ x ∘ₗ φ y).restrict hy') n) = ↑(0 n)

Tactic:
suffices ⁅y, (n : M)⁆ = 0 by simp [this]

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst✝ : LieModule.IsTrivial ↥I ↥N
hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N := fun m x_1 ↦ N.lie_mem ((mem_idealizer N).mp (h hy) m)
n : ↥N
⊢ ⁅y, ↑n⁆ = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
I : LieIdeal R L
inst✝⁴ : Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsLieAbelian ↥I
⊢ I ≤ killingCompl R L ⊤

Tactic:
intro x (hx : x ∈ I)
  simp only [mem_killingCompl, LieSubmodule.mem_top, forall_true_left]
  intro y
  rw [LieModule.traceForm_apply_apply]
  exact LieSubmodule.traceForm_eq_zero_of_isTrivial I I (by simp) _ hx

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
⊢ ((reflection hf * reflection hg) ^ (-↑m)) z =
    z +
        (Polynomial.eval t (S R ((-↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((-↑m - 1) / 2)) + Polynomial.eval t (S R ((-↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((-↑m - 1) / 2)) *
          (Polynomial.eval t (S R (-↑m / 2)) + Polynomial.eval t (S R ((-↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
| neg _ m =>

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (U R n) = eval x (U R' n)

Tactic:
by
  rw [aeval_def, eval₂_eq_eval_map, map_U]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsRootSystem
i j : ι
⊢ P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩
  ext x
  exact (P.reflectionPerm_eq_reflectionPerm_iff_of_span i j).mp h x <| by simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.coxeterWeight i j = P.coxeterWeight j i

Tactic:
simp only [coxeterWeight, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
h_unit : IsUnit (A.submatrix id ⇑e)
⊢ IsUnit A'

Tactic:
have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]

Goal state after:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
h_unit : IsUnit (A.submatrix id ⇑e)
h_det : (A.submatrix id ⇑e).det = K.subtype A'.det
⊢ IsUnit A'
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
⊢ mk' K (num A x) (den A x) = x

Tactic:
apply mk'_num_den

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ eval₂ (algebraMap A K) ((algebraMap A K) (num A x)) (p.scaleRoots ↑(den A x)) = 0

Tactic:
refine scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (aeval (mk' K (num A x) (den A x))) p = 0
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ a * (b' * (1 - (mk (I ^ (n + 1))) c)) = 1

Tactic:
calc
    _ = (a * b' - 1) * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) +
        (1 - Ideal.Quotient.mk (I ^ (n + 1)) c) := by ring
    _ = 1 := by
      rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]
      apply Ideal.mul_mem_mul hc (Ideal.mul_le_right (I := I ^ (n - 1)) _)
      simpa only [← pow_add, Nat.sub_add_cancel npos] using! hc

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N

Tactic:
induction h generalizing N with

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
b : α
x✝ : 0 < ↑b
⊢ ↑x * 0 < ↑x * ↑b

Tactic:
simpa only [mul_zero] using! WithZero.zero_lt_coe _

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
b : α
x✝ : 0 < ↑b
⊢ 0 * ↑x < ↑b * ↑x

Tactic:
simpa only [mul_zero] using! WithZero.zero_lt_coe _

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

Tactic:
use f (gcd x y)

Goal state after:
case h
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} = S ∙ f (gcd x y)
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
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) (r2 * r1) = (algebraMap O R) 1

Tactic:
rw [map_mul, map_one, hr1, hr2, Units.inv_mul]

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

Goal state before:
pp: case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R

Tactic:
exact hv.hom_inj.nontrivial

Goal state after:
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
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a : ValueGroup A K), a * 1 = a

Tactic:
rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]

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

Goal state before:
pp: 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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ (algebraMap R K) s = (algebraMap R K) (y * s) / (algebraMap R K) y

Tactic:
rwa [eq_div_iff, map_mul, mul_comm]

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

Tactic:
← sub_eq_zero,

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.Valuation.Basic

Goal state before:
pp: case inl
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) = 0
⊢ v (∑ i ∈ s, f i) = v (f j)

pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) ≠ 0
⊢ v (∑ i ∈ s, f i) = v (f j)

Tactic:
· aesop

Goal state after:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) ≠ 0
⊢ v (∑ i ∈ s, f i) = v (f j)
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : Nontrivial R
⊢ Subsingleton (PrimeSpectrum R) ↔ IsField R

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ letI := H.toField; inferInstance⟩

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : Nontrivial R
H : Subsingleton (PrimeSpectrum R)
⊢ IsField R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose ⋯)
⊢ a = 0 → (addVal R) a = ⊤

Tactic:
· rintro rfl
    exact addVal_zero

Goal state after:
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) x = (addVal R) y
hx : ¬x = 0
hy : y = 0
⊢ Associated x y

Tactic:
simp_all only [AddValuation.map_zero, associated_zero_iff_eq_zero]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = ⊤
hx : ¬x = 0
hy : y = 0
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x ϖ : R
hϖ : Irreducible ϖ
hx : ∀ (n : ℕ), ↑n ≤ (addVal R) x
⊢ x = 0

Tactic:
← addVal_eq_top_iff,

Goal state after:
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x ϖ : R
hϖ : Irreducible ϖ
hx : ∀ (n : ℕ), ↑n ≤ (addVal R) x
⊢ (addVal R) x = ⊤
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ

Tactic:
by
  set u := WithZero.unzero (Units.ne_zero γ) with hu_def
  obtain ⟨a, ⟨ha, x, hax⟩⟩ := (mem_valueGroup_iff_of_comm _).mp u.2
  have hx : 0 < v x := by
    rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
    aesop
  use x, a, hx, zero_lt_iff.mpr ha
  have ha0 : v.restrict a ≠ 0 := by simpa using ha
  rw [div_eq_iff ha0, mul_comm, ← embedding_strictMono.injective.eq_iff, map_mul,
    embedding_restrict, embedding_restrict]
  rw [← MonoidWithZeroHom.coe_ofClass, ← hax]
  congr
  rw [← WithZero.coe_unzero (Units.ne_zero γ)]
  exact Eq.refl ..

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
⊢ p.IsMaximal

Tactic:
rcases p.exists_le_maximal (Ideal.IsPrime.ne_top hpp) with ⟨q, hq, hpq⟩

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
⊢ p.IsMaximal
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] ↔ IsJacobsonRing R

Tactic:
refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] → IsJacobsonRing R
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 : ι
⊢ B.rootLength ((P.reflectionPerm i) i) = B.rootLength i

Tactic:
simp [rootLength, rootSpanMem_reflectionPerm_self]

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

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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j : ι
⊢ root j - (p (root j)) (coroot i) • root i = root ((RootPairing.equiv_of_mapsTo p root coroot i hr hp) j)

Tactic:
by
    simp [(exist_eq_reflection_of_mapsTo p root coroot i j hr).choose_spec, preReflection_apply]

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

Goal state before:
pp: case left
ι : 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
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(span S (range ⇑P.root))
⊢ (∀ (y : ↥(span S (range ⇑P.root))), ((P.posRootForm S).posForm x) y = 0) → x = 0

Tactic:
contrapose!

Goal state after:
case left
ι : 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
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(span S (range ⇑P.root))
⊢ x ≠ 0 → ∃ y, ((P.posRootForm S).posForm x) y ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case right
ι : 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
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(span S (range ⇑P.root))
⊢ (∀ (x_1 : ↥(span S (range ⇑P.root))), ((P.posRootForm S).posForm x_1) x = 0) → x = 0

Tactic:
contrapose!

Goal state after:
case right
ι : 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
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(span S (range ⇑P.root))
⊢ x ≠ 0 → ∃ x_1, ((P.posRootForm S).posForm x_1) x ≠ 0
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
⊢ P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j

Tactic:
rw [isReduced_iff]

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
⊢ (∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j) ↔
    ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
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 : ι
c : R
hc : ∏ i, (P.RootForm (P.root i)) (P.root i) = (P.RootForm (P.root i)) (P.root i) * c
⊢ ∃ y, (P.Polarization.domRestrict (P.rootSpan R)) y = c • 2 • P.Polarization (P.root i)

Tactic:
use ⟨c • 2 • P.root i, by aesop⟩

Goal state after:
case h
ι : 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 : ι
c : R
hc : ∏ i, (P.RootForm (P.root i)) (P.root i) = (P.RootForm (P.root i)) (P.root i) * c
⊢ (P.Polarization.domRestrict (P.rootSpan R)) ⟨c • 2 • P.root i, ⋯⟩ = c • 2 • P.Polarization (P.root i)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_3
ι : 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✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i = 2 • P.root j

Tactic:
← sub_eq_zero,

Goal state after:
case refine_3
ι : 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✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i - 2 • P.root j = 0
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_3
ι : 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✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i + -(2 • P.root j) = 0

Tactic:
exact hl

Goal state after: