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 : T R (- -↑n) = T R (-↑n)
ih2 : T R (-(-↑n + 1)) = T R (-↑n + 1)
⊢ T R (-(-↑n - 1)) = T R (-↑n - 1)

Tactic:
have h₁ := T_add_one R n

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
have := U_add_two R 0
  simp only [zero_add, U_one, U_zero] at this
  linear_combination this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n + 1) = X * U R n + T R (n + 1)

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    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: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n

Tactic:
have h₁ := U_eq_X_mul_U_add_T R n

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ : U R (n + 1) = X * U R n + T R (n + 1)
⊢ T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case pred
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R (-↑n) ^ 2 + S R (-↑n + 1) ^ 2 - X * S R (-↑n) * S R (-↑n + 1) = 1
⊢ S R (-↑n - 1) ^ 2 + S R (-↑n - 1 + 1) ^ 2 - X * S R (-↑n - 1) * S R (-↑n - 1 + 1) = 1

Tactic:
have h₁ := S_sub_one R (-n)
    linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih

Goal state after:
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Nontrivial R
ι : Type u_3 := Free.ChooseBasisIndex R ↥p
b₁ : Basis ι R ↥p := Free.chooseBasis R ↥p
b₂ : Basis ι A ↥(span A ↑p) := (Basis.baseChange A b₁).map (tensorEquivSpan A p)
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

Tactic:
rw [finrank_eq_card_basis b₁, finrank_eq_card_basis b₂]

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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).range = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun g : Module.Dual S N' ↦ ?_

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
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
⊢ g ∈ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).range
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
this : ¬IsFiniteLength R M
⊢ length R M = length R N + length R P

Tactic:
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this

Goal state after:
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 : length R P = ⊤
this : length R M = ⊤
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) c * (algebraMap A K) xa * (algebraMap A K) yb = (algebraMap A K) ya * (algebraMap A K) xb

Tactic:
simp only [← map_mul]

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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) (c * xa * yb) = (algebraMap A K) (ya * xb)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) c * (algebraMap A K) xb * (algebraMap A K) ya = (algebraMap A K) yb * (algebraMap A K) xa

Tactic:
simp only [← map_mul]

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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) (c * xb * ya) = (algebraMap A K) (yb * xa)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.refine_1
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
x : O
hx : I = O ∙ x
⊢ (⇑v ∘ ⇑(algebraMap O F)) x ∈ ⇑v ∘ ⇑(algebraMap O F) '' ↑I

Tactic:
refine Set.mem_image_of_mem _ ?_
      simp [hx]

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

Goal state before:
pp: case inr
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya + (algebraMap A K) xb / (algebraMap A K) yb) ≤
    max (Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya))
      (Quotient.mk'' ((algebraMap A K) xb / (algebraMap A K) yb))

Tactic:
· apply le_trans _ (le_max_right _ _)
      use c + 1
      rw [Algebra.smul_def]
      field_simp
      simp only [← map_mul, ← map_add]
      congr 1; linear_combination h

Goal state after:
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 : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1

Tactic:
intro P

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 : x ∈ I.jacobson
P : Ideal R
⊢ P ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ P
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Tactic:
intro P

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
⊢ P.IsPrime → P.jacobson = P
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ n, Associated x (ϖ ^ n)

Tactic:
have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
  obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx
  use Multiset.card fx
  have H := hfx.2
  rw [← Associates.mk_eq_mk_iff_associated] at H ⊢
  rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
  congr 1
  rw [Multiset.eq_replicate]
  simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]
  rintro _ _ _ rfl
  rw [Associates.mk_eq_mk_iff_associated]
  refine associated_of_irreducible _ ?_ hirr
  apply hfx.1
  assumption

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x : K
hx : x ≠ 0
⊢ ∃ n u, x = u • (algebraMap R K) ϖ ^ n

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x
  obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible (x := x) (by simp_all) hϖ
  obtain ⟨m, v, rfl⟩ := eq_unit_mul_pow_irreducible (by simpa using hy) hϖ
  have hϖ' : algebraMap R K ϖ ≠ 0 := by simpa using hϖ.ne_zero
  refine ⟨n - m, u / v, ?_⟩
  simp [hϖ', zpow_sub₀, div_smul_div_comm, Units.smul_def u, Units.smul_def v, Algebra.smul_def]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ m = n

Tactic:
have key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod := by
    rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]
    refine ⟨u * v⁻¹, ?_⟩
    simp only [Units.val_mul]
    rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]
  have := by
    refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)
    all_goals
      intro x hx
      obtain rfl := Multiset.eq_of_mem_replicate hx
      assumption
  simpa only [Multiset.card_replicate]

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

Goal state before:
pp: case pos.inl
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 x ≠ 0
⊢ (↑(restrict₀ (ofClass v))).toFun (x + y) ≤
    max ((↑(restrict₀ (ofClass v))).toFun x) ((↑(restrict₀ (ofClass v))).toFun y)

Tactic:
simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, coe_ofClass, h,
        reduceDIte, le_sup_iff]

Goal state after:
case pos.inl
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 x ≠ 0
⊢ (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos.inr
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
⊢ (↑(restrict₀ (ofClass v))).toFun (x + y) ≤
    max ((↑(restrict₀ (ofClass v))).toFun x) ((↑(restrict₀ (ofClass v))).toFun y)

Tactic:
simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply, coe_ofClass, h,
        reduceDIte, le_sup_iff]

Goal state after:
case pos.inr
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
⊢ ((if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v y) ⋯, ⋯⟩
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ ¬(restrict₀ (ofClass v)) x = 0

Tactic:
restrict₀_eq_zero_iff

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ ¬(ofClass v) x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
⊢ toWithBotNat (remainder x y) < toWithBotNat y

Tactic:
remainder

Goal state after:
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
⊢ toWithBotNat (if y ∣ x then 0 else x) < toWithBotNat y
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
⊢ toWithBotNat 0 < toWithBotNat y

Tactic:
rwa [toWithBotNat_zero, bot_lt_toWithBotNat_iff]

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

Goal state after:
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
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
⊢ ∀ [inst : IsDiscreteValuationRing O] {ϖ : O},
    Irreducible ϖ → ↑(maximalIdeal O) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ)}
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 ϖ → ∀ (n : ℕ), ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

Tactic:
let : IsDomain O := hv.hom_inj.isDomain

Goal state after:
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
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
⊢ ∀ [inst : IsDiscreteValuationRing O] {ϖ : O},
    Irreducible ϖ → ∀ (n : ℕ), ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ ¬x = 0

Tactic:
leadingCoeff_eq_zero

Goal state after:
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 : map (Ideal.Quotient.mk (comap C P)) p ≠ 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ ¬map (Ideal.Quotient.mk P') p = 0
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
⊢ Flat R M

Tactic:
iff_lift_lsmul_comp_subtype_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
⊢ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : torsion R M = ⊥
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)

Tactic:
intro P

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : torsion R M = ⊥
P : Ideal R
⊢ ∀ [inst : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
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
S : Type u_6
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
T : Type u_7
inst✝⁶ : CommRing T
inst✝⁵ : Algebra T S
inst✝⁴ : Algebra T R
inst✝³ : IsScalarTower T S R
inst✝² : P.IsValuedIn T
inst✝¹ : P.IsValuedIn S
inst✝ : FaithfulSMul S R
i j : ι
⊢ (algebraMap T S) (P.pairingIn T i j) = P.pairingIn S i j

Tactic:
by
  apply FaithfulSMul.algebraMap_injective S R
  rw [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq]
  simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
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
B : P.InvariantForm
i j : ι
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ P.pairing i j * (B.form (P.root j)) (P.root j) = 0 ↔ P.pairing i j = 0

Tactic:
simp [B.ne_zero j]

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

Tactic:
rcases eq_or_ne t 0 with rfl | ht

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
s : R
h₂ : s ≠ 0
h₁ : s • P.root i + 0 • P.root j = 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
ht : t ≠ 0
⊢ t ≠ 0
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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 (⇑α) β)
hα : α.IsZero
⊢ chainLength α β • x = ⁅coroot α, x⁆

pp: case neg
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 (⇑α) β)
hα : ¬α.IsZero
⊢ chainLength α β • x = ⁅coroot α, x⁆

Tactic:
· rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]

Goal state after:
case neg
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 (⇑α) β)
hα : ¬α.IsZero
⊢ chainLength α β • x = ⁅coroot α, x⁆