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

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (-↑n + 1) = X * U R (-↑n) + T R (-↑n + 1)
ih2 : U R (-↑n + 1 + 1) = X * U R (-↑n + 1) + T R (-↑n + 1 + 1)
h₁ : U R (-↑n - 1 + 2) = 2 * X * U R (-↑n - 1 + 1) - U R (-↑n - 1)
h₂ : U R (-↑n + 2) = 2 * X * U R (-↑n + 1) - U R (-↑n)
h₃ : T R (-↑n + 2) = 2 * X * T R (-↑n + 1) - T R (-↑n)
⊢ U R (-↑n - 1 + 1) = X * U R (-↑n - 1) + T R (-↑n - 1 + 1)

Tactic:
linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1

Goal state after:
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
⊢ eval (-2) (C R (↑n + 2)) = 2 * ↑↑(↑n + 2).negOnePow

Tactic:
simp only [C_add_two, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]

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.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
⊢ U = ⨆ i ∈ sU, LieModule.genWeightSpace L i

Tactic:
simp only [hU, hsU, mem_ofPred_eq, iSup_exists, iSup_and, iSup_comm (ι := H → R),
      iSup_iSup_eq_left, LinearMap.coe_sum, LinearMap.coe_smul]

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

Goal state before:
pp: case neg
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
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H ⇑α ≤ LieSubmodule.restr I H
⊢ LieSubmodule.restr I H ⊓ rootSpace H ⇑α ≤ ⨆ α, ⨆ (_ : rootSpace H ⇑↑α ≤ LieSubmodule.restr I H), rootSpace H ⇑↑α

Tactic:
· have ha := Submodule.isAtom_iff_finrank_eq_one.mpr (finrank_rootSpace_eq_one α hα)
    have : I.restr H ⊓ rootSpace H (α : H → K) = ⊥ :=
      LieSubmodule.toSubmodule_injective ((ha.not_le_iff_disjoint.mp h).symm.eq_bot)
    simp only [this, bot_le]

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

Goal state before:
pp: case calc_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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.toLinearMap x) (P.coroot i) • P.pairing i j • P.root j = (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

Tactic:
rw [← smul_comm, ← smul_assoc, map_smul]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
this : ↑(den A r) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ ↑(den A r)
⊢ q ∣ num A r ^ p.natDegree → ¬Prime q

Tactic:
dvd_num_pow

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
this : ↑(den A r) ∣ p.leadingCoeff * num A r ^ p.natDegree
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ p.natDegree
⊢ ¬Prime q
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m

Goal state after:
case add_two
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 * X * T R (↑m + 1) - T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case intro
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
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
left✝ : IsNoetherian R M
right✝ : IsArtinian R M
⊢ IsNoetherian R N ∧ IsArtinian R N

Tactic:
exact ⟨isNoetherian_of_surjective f (LinearMap.range_eq_top.mpr hf),
    isArtinian_of_surjective _ f hf⟩

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (N₁ N₂ : Submodule R R), N₁.FG → N₂.FG → N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal

Tactic:
rintro _ _ _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩

Goal state after:
case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x : R
hN₁✝ : (R ∙ x).FG
y : R
hN₂✝ : (R ∙ y).FG
⊢ (R ∙ x ⊔ R ∙ y).IsPrincipal
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : v x ≤ 1
⊢ -x ∈ {x | v x ≤ 1}

Tactic:
simpa only [Set.mem_ofPred_eq, map_neg]

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✝ b✝ : ValueGroup A K
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ e ∣ 1

Tactic:
use f

Goal state after:
case h
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
b : K
e f : A
hf : f • e • b = b
hb : ¬b = 0
⊢ 1 = e * f
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing S
inst✝² : Module S M
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S M
⊢ IsPrecomplete (Ideal.map (algebraMap R S) I) M ↔ IsPrecomplete I M

Tactic:
by
  simp [isPrecomplete_iff, ← Ideal.map_pow, ← SModEq.restrictScalars R,
    restrictScalars_map_smul_eq]

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
⊢ ∀ (a b : Ideal A), a ≤ b ∨ b ≤ a

Tactic:
intro α β

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
⊢ α ≤ β ∨ β ≤ α
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit ϖ
⊢ Associated p ϖ

pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ

Tactic:
· exact (hϖ.not_isUnit H0).elim

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : 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 : 𝒪
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h

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

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ ∃ a, I = R ∙ a

Tactic:
use p ^ Nat.find ex

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ I = R ∙ p ^ Nat.find ex
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ I ≤ span {p ^ Nat.find ex}

Tactic:
intro r hr
    by_cases hr0 : r = 0
    · simp only [hr0, Submodule.zero_mem]
    obtain ⟨n, u, rfl⟩ := H hr0
    simp only [mem_span_singleton, Units.isUnit, IsUnit.dvd_mul_right]
    apply pow_dvd_pow
    apply Nat.find_min'
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hr

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
inst✝² : KrullDimLE 0 R
inst✝¹ : IsReduced R
inst✝ : IsLocalRing R
⊢ IsField R

Tactic:
IsLocalRing.isField_iff_maximalIdeal_eq,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : KrullDimLE 0 R
inst✝¹ : IsReduced R
inst✝ : IsLocalRing R
⊢ IsLocalRing.maximalIdeal R = ⊥
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
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 y ≠ 0
H : ¬v (x + y) = 0
hx : v x = 0
⊢ (↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩ ≤ if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    Units.mk0 (v (x + y)) ⋯ ≤ Units.mk0 (v y) ⋯

Tactic:
simpa [hx, ← Units.val_le_val] using map_add_le _ (hx ▸ zero_le) (le_rfl (a := v y))

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

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ maximalIdeal R ^ Nat.find this ≤ I

Tactic:
rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]

Goal state after:
case a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ x ^ Nat.find this ∈ ↑I
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
by_cases ne_bot : maximalIdeal R = ⊥

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : CommRing O
inst✝ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
⊢ ∀ [inst : IsDiscreteValuationRing O] {ϖ : O},
    Irreducible ϖ → ↑(maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}

Tactic:
let : IsDomain O := hv.hom_inj.isDomain
  intro _ _ h
  rw [← hv.coe_span_singleton_eq_setOfPred_le_v_algebraMap, ← h.maximalIdeal_eq]

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ

Tactic:
refine (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDomain Aₘ

case refine_2
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ

case refine_3
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ

case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, (algebraMap Aₘ (FractionRing A)) y = x
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 Γ'₀
⊢ (∀ (r s : R), v s < v r ↔ v' s < v' r) ↔ ∀ {x y : R}, v x < v y ↔ v' x < v' y

Tactic:
exact forall_comm

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) 0) = 0

Tactic:
rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]

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

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 R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ P.flip.IsValuedIn S

Tactic:
rw [isValuedIn_iff, forall_comm]

Goal state after:
ι : Type u_1
R : Type u_2
S✝ : Type u_3
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 j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ ∀ (b a : ι), ∃ s, (algebraMap S R) s = P.flip.pairing a b
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
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)
⊢ (B.form ((span S (range ⇑P.root)).subtype ⟨x, hx⟩)) ((span S (range ⇑P.root)).subtype ⟨y, hy⟩) ∈
    (Algebra.linearMap S R).range

Tactic:
apply LinearMap.BilinMap.apply_apply_mem_of_mem_span
      (s := range P.root) (t := range P.root)
      (B := (LinearMap.restrictScalarsₗ S R _ _ _).comp (B.form.restrictScalars S))
    · rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
      simpa using B.exists_eq i j
    · simpa
    · simpa

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
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 : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : (P.coroot'In S i) x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (P.coroot'In S i) x * (P.coroot'In S i) x

Tactic:
use i

Goal state after:
case h
ι : 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 : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : (P.coroot'In S i) x ≠ 0
⊢ i ∈ Finset.univ ∧ 0 < (P.coroot'In S i) x * (P.coroot'In S i) x
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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ P₁.coroot i ∈ range ⇑P₂.coroot

Tactic:
use i

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ P₂.coroot i = P₁.coroot i
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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
⊢ s ≠ 0

Tactic:
rcases eq_or_ne s 0 with rfl | hs

Goal state after:
case inl
ι : 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
t : R
h₁ : 0 • P.root i + t • P.root j = 0
h₂ : 0 = 0 → t ≠ 0
⊢ 0 ≠ 0

case inr
ι : 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
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s = 0 → t ≠ 0
hs : s ≠ 0
⊢ s ≠ 0
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:
by
  rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]

Goal state after: