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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (↑k + 1) = C R (m + (↑k + 1)) + C R (m - (↑k + 1))
ih2 : C R m * C R ↑k = C R (m + ↑k) + C R (m - ↑k)
h₁ : C R (m + ↑k + 2) = X * C R (m + ↑k + 1) - C R (m + ↑k)
⊢ C R m * C R (↑k + 2) = C R (m + (↑k + 2)) + C R (m - (↑k + 2))

Tactic:
have h₂ := C_sub_two R (m - k)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (↑k + 1) = C R (m + (↑k + 1)) + C R (m - (↑k + 1))
ih2 : C R m * C R ↑k = C R (m + ↑k) + C R (m - ↑k)
h₁ : C R (m + ↑k + 2) = X * C R (m + ↑k + 1) - C R (m + ↑k)
h₂ : C R (m - ↑k - 2) = X * C R (m - ↑k - 1) - C R (m - ↑k)
⊢ C R m * C R (↑k + 2) = C R (m + (↑k + 2)) + C R (m - (↑k + 2))
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 ≠ ⊤ ↔ FiniteDimensionalOrder (Submodule R M)

Tactic:
by
  rw [Ne, length_eq_top_iff_infiniteDimensionalOrder, ← not_finiteDimensionalOrder_iff, not_not]

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
⊢ Order.height ⊤ = length R M

Tactic:
Module.length_eq_height

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Order.height ⊤ = Order.height ⊤
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 : O
hvx : v ((algebraMap O F) x) = 1
⊢ (algebraMap O F) x ≠ 0

Tactic:
simp only [← v.ne_zero_iff, hvx, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: case mp.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s)) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) (x * s))⁻¹

Tactic:
exact Or.inr
        ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩

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
f g : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
hg : g ∈ {f | IsAdicCauchy I M f}
m : ℕ
⊢ ∀ {n : ℕ}, m ≤ n → (f + g) m ≡ (f + g) n [SMOD I ^ m • ⊤]

Tactic:
n

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
f g : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
hg : g ∈ {f | IsAdicCauchy I M f}
m n : ℕ
⊢ m ≤ n → (f + g) m ≡ (f + g) 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
r : R
f : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
m : ℕ
⊢ ∀ {n : ℕ}, m ≤ n → (r • f) m ≡ (r • f) n [SMOD I ^ m • ⊤]

Tactic:
n

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
r : R
f : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
m n : ℕ
⊢ m ≤ n → (r • f) m ≡ (r • f) n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : R ∙ 0 ≠ ⊥
hQ2 : IsPrime (R ∙ 0)
⊢ False

Tactic:
apply hQ1

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : R ∙ 0 ≠ ⊥
hQ2 : IsPrime (R ∙ 0)
⊢ R ∙ 0 = ⊥
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : IsAdicCauchy I M f
⊢ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
n

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m : ℕ
⊢ ∀ {n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]

Tactic:
n

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n : ℕ
⊢ m ≤ n → f m ≡ f 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 : AdicCauchySequence I M
m : ℕ
⊢ ∀ {n : ℕ} (hmn : m ≤ n),
    (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m

Tactic:
n

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
f : AdicCauchySequence I M
m n : ℕ
⊢ ∀ (hmn : m ≤ n), (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ Ideal.span {a * g, b * g}

Tactic:
rw [e]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ Ideal.span {g}
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m : ℕ
⊢ ∀ {n : ℕ}, m ≤ n → a m ≡ a n [SMOD I ^ m • ⊤]

Tactic:
n

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
⊢ m ≤ n → a m ≡ a n [SMOD I ^ m • ⊤]
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 : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]

Tactic:
n

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 : ℕ
⊢ m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
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 := ⋯
m n : ℕ
h : m ≤ n
⊢ ∀ c ∈ range (n - m), (x * y) ^ (m + c) ∈ I ^ m

Tactic:
intro n _

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✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ (x * y) ^ (m + n) ∈ I ^ m
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hxy✝ : x * y ∈ under R P'
hxy : x ∈ under R P'
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
exact hxy

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Subsingleton R
v : Valuation R Γ₀
x : R
⊢ v x ≤ 1

Tactic:
Subsingleton.elim x 1,

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Subsingleton R
v : Valuation R Γ₀
x : R
⊢ v 1 ≤ 1
Module: Mathlib.RingTheory.KrullDimension.Zero

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

Tactic:
by
  by_contra h
  obtain ⟨p, hp, h⟩ := Ring.not_isField_iff_exists_prime.mp h
  exact hp.symm (Ideal.isPrime_bot.isMaximal'.eq_of_le h.ne_top bot_le)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring.KrullDimLE 0 R
inst✝ : IsLocalRing R
M : Submonoid R
⊢ M ≤ IsUnit.submonoid R ↔ 0 ∉ M

Tactic:
by
  have := ((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 2 rfl rfl).mp ⟨‹_›, ‹_›⟩
  exact ⟨fun h₁ h₂ ↦ not_isUnit_zero (h₁ h₂),
    fun H x hx ↦ (this x).not_left.mp fun ⟨n, hn⟩ ↦ H (hn ▸ pow_mem hx n)⟩

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

Goal state before:
pp: case refine_1.inl.refine_1
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = X
⊢ eval₂ φ ((Ideal.Quotient.mk P) X) (map (Ideal.Quotient.mk P') pX) = 0

Tactic:
rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]

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

Goal state before:
pp: case neg
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
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x

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
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ y * Exists.choose h₂ + 0 = x

pp: case neg
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
h₁ : ¬y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x

Tactic:
· rw [h₁]; ring

Goal state after:
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
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ y * Exists.choose h₂ + 0 = x

case neg
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
h₁ : ¬y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x
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 (if y ∣ x then 0 else x) < toWithBotNat y

Tactic:
split_ifs with hyx

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

case neg
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 x < toWithBotNat y
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
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
⊢ ∀ (n : ℕ), ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

Tactic:
n

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
h : Irreducible ϖ
n : ℕ
⊢ ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
⊢ ∀ {p : Ideal Rₘ}, p ≠ ⊥ → p.IsPrime → p.IsMaximal

Tactic:
intro p hp0 hpp

Goal state after:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
⊢ p.IsMaximal
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ∀ y ∈ M, x * y ∈ M
⊢ M.FG

Tactic:
apply Submodule.FG.map

Goal state after:
case pos.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := ⋯
x : K := ⋯
M : Submodule R K := ⋯
ha₃ : (algebraMap R K) a ≠ 0
hx : ∀ y ∈ M, x * y ∈ M
⊢ Submodule.FG (maximalIdeal R)
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ¬IsField R
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
have : finrank (ResidueField R) (CotangentSpace R) = 1 ↔
      finrank (ResidueField R) (CotangentSpace R) ≤ 1 := by
    simp [Nat.le_one_iff_eq_zero_or_eq_one, finrank_cotangentSpace_eq_zero_iff, h]
  rw [this]
  have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h
  convert! tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R
  · exact ⟨fun _ ↦ inferInstance, fun h ↦ { h with not_a_field' := this }⟩
  · exact ⟨fun h P h₁ h₂ ↦ h.unique ⟨h₁, h₂⟩ ⟨this, inferInstance⟩,
      fun H ↦ ⟨_, ⟨this, inferInstance⟩, fun P hP ↦ H P hP.1 hP.2⟩⟩

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]
  exact P.exists_value

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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
⊢ ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j -
        (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype
                (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯)
              ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
            ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } j) •
          { toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    ↑({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } ((P.reflectionPerm i) j))

Tactic:
simpa [algebra_compatible_smul L] using P.reflectionPerm_coroot i j

Goal state after:
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 ι
m : M
h : P.Polarization m = 0
⊢ (P.flip.toLinearMap ∘ₗ P.Polarization) m = 0

Tactic:
by simp [h]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
⊢ v.IsEquiv v'

Tactic:
by
  intro x y
  obtain rfl | hy := eq_or_ne y 0
  · simp
  · rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀] <;>
      rwa [zero_lt_iff, ne_zero_iff]

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

Goal state before:
pp: case neg.mpr.inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v' x⁻¹ = 1
h_1 : ¬v x = 1
h_2 : 1 < v x
⊢ False

Tactic:
exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))

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✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan R, (P.RootForm n) x = 0
⊢ ∃ u ∈ P.rootSpan R, ∃ v ∈ LinearMap.ker P.RootForm, u + v = y

Tactic:
← Submodule.mem_sup,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan R, (P.RootForm n) x = 0
⊢ y ∈ P.rootSpan R ⊔ LinearMap.ker P.RootForm
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
⊢ LinearIndependent R b

Tactic:
by
    refine (LinearMap.linearIndependent_iff_of_injOn _ (subtype_injective _).injOn).mpr <|
      linearIndependent_of_top_le_span_of_card_eq_finrank (b := fun i ↦ ⟨b i, subset_span ⟨i, rfl⟩⟩)
        (fun ⟨_, _⟩ _ ↦ (subtype_injective _).mem_set_image.mp ?_) hc
    rwa [← map_coe, ← span_image, ← Set.range_comp]

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : i = j
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2

Tactic:
by simp [h]

Goal state after: