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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ (if hα : α = 0 then 0 else (Nat.find ⋯).pred) + 1 = Nat.find ⋯

Tactic:
dif_neg hα

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ (Nat.find ⋯).pred + 1 = Nat.find ⋯
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
this : tail.degree < ↑m
⊢ P - head ∈ degreeLT R m

Tactic:
rwa [Polynomial.mem_degreeLT]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ (reflection h) y ∈ p

Tactic:
simpa only [reflection_apply, p.sub_mem_iff_right hy] using p.smul_mem (f y) hx

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : 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
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e ∪ range b.f)
hy✝ : v ∈ lieSpan R L (range b.e ∪ range b.f)
hu : u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv : v ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅u, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| lie u v _ _ hu hv =>

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
⊢ ((killingForm K L) e) f ≠ 0

Tactic:
have := ht.h_ne_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
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
this : ↑h ≠ 0
⊢ ((killingForm K L) e) f ≠ 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : 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
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
⊢ ⁅u, v⁆ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
| lie u v _ _ hu hv =>

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'
f : R →+* R'
n : ℤ
⊢ map f (U R n) = U R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

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

Tactic:
let f := LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R)
      (FaithfulSMul.algebraMap_injective S R) p hp

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

Goal state before:
pp: case h
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ ((algebraMap A K) ↑(den A x))⁻¹ * (algebraMap A K) (num A x) = mk' K (num A x) (den A x)

Tactic:
apply mul_left_cancel₀ d_ne_zero

Goal state after:
case h
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ (algebraMap A K) ↑(den A x) * (((algebraMap A K) ↑(den A x))⁻¹ * (algebraMap A K) (num A x)) =
    (algebraMap A K) ↑(den A x) * mk' K (num A x) (den A x)
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
f : M →ₗ[R] N
H : IsFiniteLength R N
hf : Function.Injective ⇑f
⊢ IsFiniteLength R M

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢
  cases H
  exact ⟨isNoetherian_of_injective f hf, isArtinian_of_injective f hf⟩

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
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
⊢ length R M ≠ ⊤

Tactic:
rw [length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian]
  exact ⟨‹_›, ‹_›⟩

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
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ r.last = ⊤

Tactic:
simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P

Tactic:
· have := mt (IsFiniteLength.of_surjective · hg) hP
    rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
    rw [hP, this, add_top]

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
A : Type u_5
inst✝³ : Ring A
inst✝² : SMul A R
inst✝¹ : Module A M
inst✝ : IsScalarTower A R M
p : Submodule R M
⊢ Module.length R ↥p ≤ Module.length A ↥(restrictScalars A p)

Tactic:
rw [← WithBot.coe_le_coe, Module.coe_length, Module.coe_length]
  exact Order.krullDim_le_of_orderEmbedding (restrictScalarsEmbedding A R p)

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
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Module.length R (M ⧸ p) < Module.length R M

Tactic:
Module.length_quotient,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Order.coheight p < Module.length R M
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, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Tactic:
constructor <;> rintro ⟨x, hx⟩
  · refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
    · refine Set.mem_image_of_mem _ ?_
      simp [hx]
    · intro y hy
      simp only [Function.comp_apply, hx, Ideal.submodule_span_eq, Set.mem_image,
        SetLike.mem_coe, Ideal.mem_span_singleton] at hy
      obtain ⟨y, hy, rfl⟩ := hy
      exact le_of_dvd hv hy
  · obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
    refine ⟨a, ?_⟩
    ext b
    simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton]
    exact ⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩

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 : A
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
obtain ⟨c, h | h⟩ := PreValuationRing.cond a (1 - a)

Goal state after:
case inl
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
a c : A
h : a * c = 1 - a
⊢ IsUnit a ∨ IsUnit (1 - a)

case inr
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
a c : A
h : (1 - a) * c = a
⊢ IsUnit a ∨ IsUnit (1 - a)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = γ
right✝ : γ < 1
⊢ v ((algebraMap (↥v.integer) K) y) ≤ min 1 γ

Tactic:
rw [h]
      exact hy

Goal state after:
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
⊢ 0 ∈ {f | IsAdicCauchy I M f}

Tactic:
intro _ _ _

Goal state after:
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
m✝ n✝ : ℕ
a✝ : m✝ ≤ n✝
⊢ 0 m✝ ≡ 0 n✝ [SMOD I ^ m✝ • ⊤]
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
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
⊢ IsAdicCauchy I M f

Tactic:
rwa [isAdicCauchy_iff]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsDiscreteValuationRing R

Tactic:
rw [iff_pid_with_one_nonzero_prime]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
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
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
this : (1 - x * y) * f n - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n

Tactic:
by
    convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
    ring

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
⊢ 0 = ⊥

Tactic:
Ideal.zero_eq_bot

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ
⊢ Module.length R (R ⧸ maximalIdeal R ^ n) = ↑n

Tactic:
Module.length_quotient,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ
⊢ Order.coheight (maximalIdeal R ^ n) = ↑n
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✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
⊢ (↑(restrict₀ (ofClass v))).toFun (x + y) ≤
    max ((↑(restrict₀ (ofClass v))).toFun x) ((↑(restrict₀ (ofClass v))).toFun y)

Tactic:
by_cases H : v x ≠ 0 ∨ v y ≠ 0
    · rcases H with h | h
      all_goals simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, coe_ofClass, h,
        reduceDIte, le_sup_iff]
      all_goals split_ifs with H
      · simp [H]
      · simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk, ← Units.val_le_val,
          Units.val_mk0]
        split_ifs with hy
        · simpa [hy] using map_add_le _ (le_rfl (a := v x)) (hy ▸ zero_le)
        · simp [hy, ← Units.val_le_val]
      · simp [H]
      · simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk]
        split_ifs with hx
        · simpa [hx, ← Units.val_le_val] using map_add_le _ (hx ▸ zero_le) (le_rfl (a := v y))
        · simp [hx, ← Units.val_le_val]
    · simp only [ne_eq, not_or, Decidable.not_not] at H
      simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply,
        MonoidWithZeroHom.coe_ofClass, H, ↓reduceDIte, max_self, nonpos_iff_eq_zero]
      replace H : v (x + y) = 0 :=
        le_antisymm (map_add_le _ (le_of_eq H.1) (le_of_eq H.2)) zero_le
      simp [H]

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

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

Tactic:
rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_one, OneMemClass.coe_one,
    associatesEquivIsPrincipal_map_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
⊢ I.jacobson = I

Tactic:
suffices h : J.jacobson = J by
    replace h := congrArg (comap (Polynomial.mapRingHom i)) h
    rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h
    refine le_antisymm ?_ le_jacobson
    exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
⊢ J.jacobson = J
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
⊢ IsSMulRegular M r

Tactic:
have h := Flat.rTensor_preserves_injective_linearMap (M := M)
    (toSpanSingleton R R r) <| hr.right

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
⊢ IsSMulRegular M r
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
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:
← restrict_eq_zero_iff

Goal state after:
case pos
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.restrict a = 0
⊢ h.orderMonoidIso (v.restrict a) = w.restrict a
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 : ι
⊢ (4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i

Tactic:
rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
    ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]

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

Goal state before:
pp: case weightMap
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : M
⊢ f.weightMap x = g.weightMap x

Tactic:
dsimp [coweightHom] at hfg

Goal state after:
case weightMap
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : M
⊢ f.weightMap x = g.weightMap x
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
q : Submodule R M
⊢ q ∈ P.invtRootSubmodule ↔ ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)

Tactic:
by
  simp [invtRootSubmodule]

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

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.invtRootSubmodule

Tactic:
by
  simp [invtRootSubmodule]

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

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.invtRootSubmodule

Tactic:
by
  simp [invtRootSubmodule]

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

Goal state before:
pp: case coweightMap
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : N
⊢ f.coweightMap x = g.coweightMap x

Tactic:
dsimp [coweightHom] at hfg

Goal state after:
case coweightMap
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : N
⊢ f.coweightMap x = g.coweightMap x
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
dsimp [coweightHom] at hfg

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x