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

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ ↑n < ↑(n + 2)

Tactic:
norm_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
this : (2 * X * U R (↑n + 1)).degree = ↑(n + 2)
⊢ n < n + 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : ↑m ≠ -1
⊢ ↑m = ↑((↑m + 1).natAbs - 1)

Tactic:
norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ ↑m = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)

Tactic:
norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
⊢ leadingCoeff 2 = 2

Tactic:
rw [← C_ofNat, leadingCoeff_C]

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

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ 2 * 1 * 2 ^ (n + 1) = 2 ^ (n + 2)

Tactic:
norm_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ ↑(2 * 1 * 2 ^ (n + 1)) = ↑(2 ^ (n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R (↑n + 1)).degree

Tactic:
norm_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R ↑(n + 1)).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ ↑n < ↑(n + 1) + 1

Tactic:
norm_cast

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ n < n + 1 + 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 • T R 1 ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 1)

Tactic:
norm_cast

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 • T R 1 ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R (↑n + 2) + U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))

Tactic:
norm_cast

Goal state after:
case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R ↑(n + 2) + U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
      ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]

Tactic:
intro i

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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
i : Fin (Nat.succ 0).succ.succ
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] i ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      i
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (C R (↑n + 1)) = 2 * ↑↑(↑n + 1).negOnePow
ih2 : eval (-2) (C R ↑n) = 2 * ↑↑(↑n).negOnePow
⊢ 2 * (2 * ↑↑(↑n).negOnePow) - 2 * ↑↑(↑n).negOnePow = 2 * ↑↑((↑n).negOnePow * (-1) ^ 2)

Tactic:
norm_cast

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (C R (↑n + 1)) = 2 * ↑↑(↑n + 1).negOnePow
ih2 : eval (-2) (C R ↑n) = 2 * ↑↑(↑n).negOnePow
⊢ ↑(2 * (2 * ↑(↑n).negOnePow) - 2 * ↑(↑n).negOnePow) = ↑(2 * ↑((↑n).negOnePow * (-1) ^ 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (S R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * (↑(↑n + 1) + 1)
ih2 : eval (-2) (S R ↑n) = ↑↑(↑n).negOnePow * (↑↑n + 1)
⊢ -(2 * (↑↑((↑n).negOnePow * Int.negOnePow 1) * (↑n + 1 + 1))) - ↑↑(↑n).negOnePow * (↑n + 1) =
    ↑↑((↑n).negOnePow * (-1) ^ 2) * (↑n + 2 + 1)

Tactic:
norm_cast

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (S R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * (↑(↑n + 1) + 1)
ih2 : eval (-2) (S R ↑n) = ↑↑(↑n).negOnePow * (↑↑n + 1)
⊢ ↑(-(2 * (↑((↑n).negOnePow * Int.negOnePow 1) * ↑(n + 1 + 1))) - ↑(↑n).negOnePow * ↑(n + 1)) =
    ↑(↑((↑n).negOnePow * (-1) ^ 2) * ↑(n + 2 + 1))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (S R (-↑n)) = ↑↑(-↑n).negOnePow * (↑(-↑n) + 1)
ih2 : eval (-2) (S R (-↑n + 1)) = ↑↑(-↑n + 1).negOnePow * (↑(-↑n + 1) + 1)
⊢ -(2 * (↑↑(↑n).negOnePow * (-↑n + 1))) - ↑↑((↑n).negOnePow * Int.negOnePow 1) * (-↑n + 1 + 1) =
    -(↑↑((↑n).negOnePow * Int.negOnePow 1) * ↑n)

Tactic:
norm_cast

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (S R (-↑n)) = ↑↑(-↑n).negOnePow * (↑(-↑n) + 1)
ih2 : eval (-2) (S R (-↑n + 1)) = ↑↑(-↑n + 1).negOnePow * (↑(-↑n + 1) + 1)
⊢ -(2 * (↑↑(↑n).negOnePow * (-↑n + 1))) - ↑↑((↑n).negOnePow * Int.negOnePow 1) * (-↑n + 1 + 1) =
    ↑(-(↑((↑n).negOnePow * Int.negOnePow 1) * ↑n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ (S R (↑n + 2)).comp (2 * X) = 2 * X * U R (↑n + 1) - U R ↑n

Tactic:
S_add_two,

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ (X * S R (↑n + 1) - S R ↑n).comp (2 * X) = 2 * X * U R (↑n + 1) - U R ↑n
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_2
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
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ ↑↑(corootSpace ⇑α)
x_neg : L
hx_neg : x_neg ∈ ↑(genWeightSpace L (-⇑α))
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
hx_αneg : c₁ • e + x_neg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
hx : c₁ • e + x_neg + ↑H.toLieSubmodule.incl y ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ c₁ • e + x_neg + ↑H.toLieSubmodule.incl y ∈ sl2SubmoduleOfRoot hα

Tactic:
obtain ⟨c₂, rfl⟩ := aux (Weight.IsNonZero.neg hα) hx_neg hfα ht.f_ne_zero

Goal state after:
case refine_2
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
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ ↑↑(corootSpace ⇑α)
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
c₂ : K
hx_neg : c₂ • f ∈ ↑(genWeightSpace L (-⇑α))
hx_αneg : c₁ • e + c₂ • f ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
hx : c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl y ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ c₁ • e + c₂ • f + ↑H.toLieSubmodule.incl y ∈ sl2SubmoduleOfRoot hα
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (↑n + 1)) = S R' (↑n + 1)
ih2 : map f (S R ↑n) = S R' ↑n
⊢ map f (S R (↑n + 2)) = S R' (↑n + 2)

Tactic:
S_add_two,

Goal state after:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (↑n + 1)) = S R' (↑n + 1)
ih2 : map f (S R ↑n) = S R' ↑n
⊢ map f (X * S R (↑n + 1) - S R ↑n) = X * S R' (↑n + 1) - S R' ↑n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ ↑↑n • U R (↑n - 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)

Tactic:
norm_cast

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ n • U R (Int.subNatNat n 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
y : M
⊢ ↑u y = (LinearMap.id + LinearMap.smulRight (f - g) x) y

Tactic:
simp only [u, reflection_apply, hg₁, two_smul, LinearEquiv.coe_toLinearMap_mul,
      LinearMap.id_coe, LinearEquiv.coe_coe, Module.End.mul_apply, LinearMap.add_apply, id_eq,
      LinearMap.coe_smulRight, LinearMap.sub_apply, map_sub, map_smul, sub_add_cancel_left,
      smul_neg, sub_neg_eq_add, sub_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
y : M
⊢ y - g y • x + f y • x = y + (f y • x - g y • x)
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 : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0

Tactic:
intro i

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 : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
i : ι
⊢ ∀ {j : ι}, P.pairing i j = 0 → P.pairing j i = 0
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 * 2 = 4

Tactic:
norm_cast

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ ∀ (i : Fin (s.length + 1)), IsFiniteLength R ↥(s.toFun i)

Tactic:
intro i

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin (s.length + 1)
⊢ IsFiniteLength R ↥(s.toFun i)
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✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (a * 1) a

Tactic:
rw [mul_one]

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

Goal state before:
pp: case mk.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✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
hbc :
  Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

Tactic:
obtain ⟨d, hd⟩ := hbc

Goal state after:
case mk.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✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
d : A
hd : d • (a * b) = a * c
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
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
I : Ideal O
⊢ Submodule.IsPrincipal I ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
rw [isPrincipal_iff_exists_isGreatest hv]
  constructor <;> rintro ⟨x, hx⟩
  · obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
    refine ⟨a, ?_⟩
    ext b
    simp only [SetLike.mem_coe, mem_ofPred_eq]
    constructor <;> intro h
    · exact hx.right (Set.mem_image_of_mem _ h)
    · rw [le_iff_dvd hv] at h
      exact Ideal.mem_of_dvd I h ha
  · refine ⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩
    · simp [hx]
    · simp [hx, mem_upperBounds]

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

Goal state before:
pp: case mp.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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) (y * s) / (algebraMap R K) y)⁻¹

Tactic:
· exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩

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

Goal state before:
pp: case inl
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case inr
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
    use c; exact Or.inr hc.symm

Goal state after:
case inr
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)
⊢ ∃ c, a * c = b ∨ b * c = a
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}
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
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⟩⟩)

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 ∈ (Ideal.comap (algebraMap R S) P').jacobson
⊢ x ∈ Ideal.comap (algebraMap R S) P'
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 : ι), x ∈ S i

Tactic:
intro i

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 : ι
⊢ 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
x : R
h0 : v x ≠ 0
h1 : v x ≠ 1
⊢ Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueMonoid

Tactic:
Submonoid.nontrivial_iff_exists_ne_one

Goal state after:
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
x : R
h0 : v x ≠ 0
h1 : v x ≠ 1
⊢ ∃ x ∈ (MonoidWithZeroHom.ofClass v).valueMonoid, x ≠ 1
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | IsSquare x} = sumSq R

Tactic:
refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)

Goal state after:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ sumSq R
⊢ x ∈ closure {x | IsSquare x}
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
i : ι
⊢ (B.form (P.root i)) (P.root i) ≠ 0

Tactic:
obtain ⟨s, hs, hs'⟩ := B.exists_pos_eq i
  simpa [← hs'] using hs.ne'

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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ root ⋯.choose = root j

Tactic:
rw [(exist_eq_reflection_of_mapsTo p root coroot i _ h).choose_spec,
    (exist_eq_reflection_of_mapsTo p root coroot i j h).choose_spec]

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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ (preReflection (root i) (p.flip (coroot i))) ((preReflection (root i) (p.flip (coroot i))) (root j)) = root j
Module: Mathlib.RingTheory.Valuation.Basic

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

Tactic:
rw [(v.restrict_eq_mk ha)]

Goal state after:
case neg
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : ¬v a = 0
⊢ h.orderMonoidIso ↑(valueGroup.mk (ofClass v) 1 a ⋯ ha) = w.restrict a