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

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs (l - k) H.toLieSubmodule = H.toLieSubmodule

Tactic:
LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ H.toLieSubmodule = H.toLieSubmodule
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
⊢ ((B.dualBasis hB b).repr x) i = (B x) (b i)

Tactic:
have := b.finiteDimensional_of_finite
  rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
⊢ x ∈ W ⊓ ker B

Tactic:
rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩
    constructor
    · simp [hx]
    · simpa

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset

Tactic:
rw [Finset.image, Multiset.map_toEnumFinset_fst]

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
⊢ ((((consEquiv.trans v.optionCongr).trans consEquiv.symm).trans (cast ⋯).symm) x).fst = f x.fst

Tactic:
by
        simp only [consEquiv, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
            Equiv.coe_fn_symm_mk]
        split <;> simp_all

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
⊢ f.factor ∣ f

Tactic:
by
  by_cases hf2 : f = 0; · rw [hf2]; exact dvd_zero _
  rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
  exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
              map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                f.removeFactor).roots.toFinset =
    ⊤

Tactic:
roots_mul hmf0,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ↑((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                (X - C (AdjoinRoot.root f.factor))).roots +
            (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                f.removeFactor).roots).toFinset =
    ⊤
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
v : ι → R
n : ι → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
this : ∀ (i : ι), (A ^ ⨆ j, n j) i = 0
⊢ (Aᵀ ^ ⨆ j, n j) *ᵥ v = 0

Tactic:
simp [mulVec_eq_sum, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
f.mem_genEigenspace

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ ((f - μ • 1) ^ l).ker
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: case add
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
n₁ : ℕ
hn₁ : ((toEnd K L M) x ^ n₁) m₁ = 0
n₂ : ℕ
hn₂ : ((toEnd K L M) x ^ n₂) m₂ = 0
⊢ ∃ n, ((toEnd K L M) x ^ n) (m₁ + m₂) = 0

Tactic:
refine ⟨max n₁ n₂, ?_⟩

Goal state after:
case add
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m m₁ m₂ : M
hm₁ : m₁ ∈ ⨆ i, genWeightSpace M ⇑i
hm₂ : m₂ ∈ ⨆ i, genWeightSpace M ⇑i
n₁ : ℕ
hn₁ : ((toEnd K L M) x ^ n₁) m₁ = 0
n₂ : ℕ
hn₂ : ((toEnd K L M) x ^ n₂) m₂ = 0
⊢ ((toEnd K L M) x ^ max n₁ n₂) (m₁ + m₂) = 0
Module: Mathlib.LinearAlgebra.FiniteSpan

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e) Φ Φ
e' : ↑Φ ≃ ↑Φ := BijOn.equiv (⇑e) he
this : Finite ↑Φ
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun x ↦ e' * x) k 1
m : M
hm : m ∈ span R Φ
x y : M
x✝¹ : x ∈ span R Φ
x✝ : y ∈ span R Φ
hx : (e ^ k) x = x
hy : (e ^ k) y = y
⊢ (e ^ k) (x + y) = x + y

Tactic:
by simp [map_add, hx, hy]

Goal state after:
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
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ 2 •
      (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
        ((traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
congr 2

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:
rw [pow_add, pow_add]

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 * 2 ^ 1)) = ↑(2 ^ n * 2 ^ 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
C_sub_one,

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

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

Tactic:
C_sub_one,

Goal state after:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-↑n)) = C R' (-↑n)
ih2 : map f (C R (-↑n + 1)) = C R' (-↑n + 1)
⊢ map f (X * C R (-↑n) - C R (-↑n + 1)) = X * C R' (-↑n) - C R' (-↑n + 1)
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
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
← finite_coe_iff

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 ↑Φ
hx : x ∈ 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)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case succ
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
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this :
  ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R]
    ↥(Submodule.map (s.toFun i.succ).subtype (Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)))
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
Submodule.map_comap_subtype,

Goal state after:
case succ
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
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : (s.toFun i.castSucc, s.toFun i.succ) ∈ {(x, y) | JordanHolderLattice.IsMaximal x y} := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this : ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] ↥(s.toFun i.succ ⊓ s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

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

Tactic:
norm_cast at h ⊢; gcongr

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
a b : α
h : ↑a < ↑b
⊢ ↑a * ↑x < ↑b * ↑x

Tactic:
norm_cast at h ⊢; gcongr

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑x * ↑a ≤ ↑x * ↑b

Tactic:
norm_cast at h ⊢; gcongr

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑a * ↑x ≤ ↑b * ↑x

Tactic:
norm_cast at h ⊢; gcongr

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
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
Module.length_ne_top_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsFiniteLength R M ↔ IsFiniteLength R M
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
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
g : M →ₗ[R] P
hg : Function.Surjective ⇑g
⊢ length R P ≤ length R M

Tactic:
rw [Module.length_eq_add_of_exact (LinearMap.ker g).subtype g (Submodule.subtype_injective _) hg
    (LinearMap.exact_subtype_ker_map g)]
  exact le_add_self

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

pp: case inr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
· cases nonempty_fintype ι
    simp [(Finsupp.linearEquivFunOnFinite R M ι).length_eq]

Goal state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M
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
ι : Type u_5
h✝ : Infinite ι
a✝ : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
⊢ ↑m ≤ length R (ι →₀ M)

Tactic:
have : length R (s →₀ M) = ↑m * length R M := by
    simp [(Finsupp.linearEquivFunOnFinite R M _).length_eq, hs]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
a✝ : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (↥s →₀ M) = ↑m * length R M
⊢ ↑m ≤ length R (ι →₀ M)
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 ((algebraMap O R) x * (algebraMap O R) ↑u⁻¹) ≤ v ((algebraMap O R) x) * 1

Tactic:
v.map_mul,

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) x) * v ((algebraMap O R) ↑u⁻¹) ≤ v ((algebraMap O R) x) * 1
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 z : O
⊢ v ((algebraMap O R) x * (algebraMap O R) z) ≤ v ((algebraMap O R) x) * 1

Tactic:
v.map_mul,

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
hv : v.Integers O
x z : O
⊢ v ((algebraMap O R) x) * v ((algebraMap O R) z) ≤ v ((algebraMap O R) x) * 1
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) y)

Tactic:
v.map_mul,

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) y)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) y)

Tactic:
v.map_mul,

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) y)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤ ^ n • ⊤]

Tactic:
rw [Ideal.top_pow, top_smul]
      exact SModEq.top

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _
  tfae_have 1 ↔ 3 := iff_dvd_total
  tfae_have 1 ↔ 4 := iff_ideal_total
  tfae_have 1 ↔ 5 := iff_local_bezout_domain
  tfae_finish

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ HasUnitMulPowIrreducibleFactorization R

Tactic:
refine ⟨p, hp, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P

Tactic:
rw [← h P hP.right, jacobson, mem_sInf]

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | P ≤ J ∧ J.IsMaximal} → x ∈ I
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, v (f i) ≤ g
⊢ v (∑ i ∈ s, f i) ≤ g

Tactic:
classical
  refine Finset.induction_on s (fun _ => v.map_zero ▸ zero_le) (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)

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

Goal state before:
pp: 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
m n : ℕ
h : m ≤ n
⊢ ∑ i ∈ range m, (x * y) ^ i - (∑ x_1 ∈ range m, (x * y) ^ x_1 + ∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1)) ∈ I ^ m

Tactic:
← sub_sub,

Goal state after:
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
m n : ℕ
h : m ≤ n
⊢ ∑ i ∈ range m, (x * y) ^ i - ∑ x_1 ∈ range m, (x * y) ^ x_1 - ∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x - y) = v (x + -y)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x + -y) = v (x + -y)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x ≤ g
hy : v y ≤ g
⊢ v (x - y) ≤ g

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x ≤ g
hy : v y ≤ g
⊢ v (x + -y) ≤ g
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x < g
hy : v y < g
⊢ v (x - y) < g

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : v x < g
hy : v y < g
⊢ v (x + -y) < g
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h.succ
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
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ 1 - (1 + (x * y) ^ (n✝ + 1)) ∈ I ^ (n✝ + 1)

Tactic:
← sub_sub,

Goal state after:
case h.succ
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
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ 1 - 1 - (x * y) ^ (n✝ + 1) ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
hy : v y = 0
⊢ v (x - y) = v y

Tactic:
simpa [*] using map_sub v x y

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1

Tactic:
simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h

Goal state after: