mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ x ∈ ↑I

Tactic:
simp [hx]

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

Goal state before:
pp: case mpr.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 = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ x ∈ ↑I

Tactic:
simp [hx]

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
c : R
f : (n : ℕ) → M ⧸ I ^ n • ⊤
hf : f ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) ((c • f) n) = (c • f) m

Tactic:
rw [Pi.smul_apply, Pi.smul_apply, map_smul, hf hmn]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
x : M
hx : x = 0
⊢ (of I M) x = 0

Tactic:
simp [hx]

Goal state after:
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
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ maximalIdeal R = ⊥

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v y ≠ 0
H : ¬v (x + y) = 0
⊢ ((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) ⋯, ⋯⟩

Tactic:
simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk]

Goal state after:
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v y ≠ 0
H : ¬v (x + y) = 0
⊢ (↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩ ≤ if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    Units.mk0 (v (x + y)) ⋯ ≤ Units.mk0 (v y) ⋯
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
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I J : Ideal R
⊢ { toFun := fun I ↦ OrderDual.toDual ((addVal R) (generator I)),
          invFun := fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n), left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ OrderDual.toDual ((addVal R) (generator I)),
          invFun := fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n), left_inv := ⋯,
          right_inv := ⋯ }
        J ↔
    I ≤ J

Tactic:
by
    simp [addVal_le_iff_dvd, ← span_singleton_le_span_singleton]

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

Goal state before:
pp: case refine_1.inl.refine_2
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
⊢ (map (Ideal.Quotient.mk P') pX).leadingCoeff ∈ M

Tactic:
use 1
        simp only [P', pow_one]

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

Goal state before:
pp: case coe.coe
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : (addVal R) x = ↑vx
vy : ℕ
hvy : (addVal R) y = ↑vy
⊢ ↑vx ≤ ↑vy ↔ x ∣ y

Tactic:
| coe vy =>

Goal state after:
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' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
by
  by_cases h : IsField R
  · let _ := h.toField
    exact ⟨0, by simp [(eq_bot_or_eq_top I).resolve_left hI]⟩
  classical
  obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
  by_cases hI' : I = ⊤
  · use 0; rw [pow_zero, hI', Ideal.one_eq_top]
  have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
    (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
  have : x ≠ 0 := by
    rintro rfl
    apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
    simp [hx]
  have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
  have H' : ∀ r : R, r ≠ 0 → r ∈ nonunits R → ∃ n : ℕ, Associated (x ^ n) r := by
    intro r hr₁ hr₂
    obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_isUnit_iff_exists_factors_eq r hr₁).mp hr₂
    have : ∀ b ∈ f, Associated x b := by
      intro b hb
      exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
    clear hr₁ hr₂ hf₁
    induction f using Multiset.induction with
    | empty => exact (hf₂ rfl).elim
    | cons fa fs fh => ?_
    rcases eq_or_ne fs ∅ with (rfl | hf')
    · use 1
      rw [pow_one, Multiset.prod_cons, Multiset.empty_eq_zero, Multiset.prod_zero, mul_one]
      exact this _ (Multiset.mem_cons_self _ _)
    · obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)
      use n + 1
      rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]
      exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn
  have : ∃ n : ℕ, x ^ n ∈ I := by
    obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by
      by_contra! h; apply hI; rw [eq_bot_iff]; exact h
    obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
    use n
    rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
  use Nat.find this
  apply le_antisymm
  · change ∀ s ∈ I, s ∈ _
    by_contra! ⟨s, hs₁, hs₂⟩
    apply hs₂
    by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _
    obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)
    rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢
    apply Ideal.pow_le_pow_right (Nat.find_min' this hs₁)
    apply Ideal.pow_mem_pow
    exact (H _).mpr (dvd_refl _)
  · rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
    exact Nat.find_spec this

Goal state after:
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
hx : x = 0
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

Tactic:
simp [hx]

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✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
⊢ False

Tactic:
rcases eq_or_ne x 0 with rfl | hx0 <;>
  simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: case neg.succ
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
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, b ∉ Ideal.span {a} := by
    by_contra! h'; rw [Nat.find_eq_iff] at hn; exact hn.2 n n.lt_succ_self fun x hx => h' x hx

Goal state after:
case neg.succ
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}
⊢ Submodule.IsPrincipal (maximalIdeal R)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case h
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : v ↑x < 1
⊢ ↑x ≠ 0 ∧ v ↑x < 1

Tactic:
simp [hx]

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

Goal state before:
pp: case neg.succ
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
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
let K := FractionRing R

Goal state after:
case neg.succ
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
⊢ Submodule.IsPrincipal (maximalIdeal R)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
⊢ 0 < v₁ x ↔ 0 < v₂ x

Tactic:
by
  rw [zero_lt_iff, zero_lt_iff, h.eq_zero.ne]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ (algebraMap (R ⧸ P') (Localization M)).IsIntegral

Tactic:
exact (algebraMap (R ⧸ P') (Localization M)).isIntegral_of_surjective
          (IsField.localization_map_bijective hM ((Quotient.maximal_ideal_iff_isField_quotient _).mp
            (isMaximal_comap_C_of_isMaximal P hP'))).2

Goal state after:
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✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ Flat R M

Tactic:
IsDedekindDomain.flat_iff_torsion_eq_bot,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ torsion R 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
⊢ ⨅ i, LinearMap.ker (P.root' i) = (span R (range P.root')).dualCoannihilator

Tactic:
← rootSpan_dualAnnihilator_map_eq,

Goal state after:
ι : 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
⊢ ⨅ i, LinearMap.ker (P.root' i) = Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
L : Type u_8
inst✝⁶ : Field L
inst✝⁵ : Module L M
inst✝⁴ : Module L N
Q : RootPairing ι L M N
inst✝³ : Q.IsRootSystem
inst✝² : Finite ι
inst✝¹ : CharZero L
inst✝ : Q.IsCrystallographic
⊢ finrank ℤ ↥(Q.rootSpan ℤ) = finrank L M

Tactic:
let _i : Module ℚ M := .compHom M (algebraMap ℚ L)
  let _i : Module ℚ N := .compHom N (algebraMap ℚ L)
  have _i : IsAddTorsionFree M := .of_isTorsionFree L M
  rw [← Submodule.finrank_span_eq_finrank_span ℤ ℚ, ← Q.finrank_rootSpanIn ℚ]

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 ι
x✝¹ x✝ : M
⊢ ((P.flip.toLinearMap ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) x✝

Tactic:
simp [rootForm_apply_apply, RootPairing.flip]

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
S : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x y : ↥(P.rootSpan S)
⊢ (algebraMap S R) (((P.RootFormIn S) x) y) = (P.RootForm ↑x) ↑y

Tactic:
by
  simp [RootFormIn, rootForm_apply_apply]

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

Goal state before:
pp: case 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 y : K
hy : y ≠ 0
⊢ 0 < v' y

Tactic:
rwa [zero_lt_iff, ne_zero_iff]

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

Goal state before:
pp: case 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 y : K
hy : y ≠ 0
⊢ 0 < v y

Tactic:
rwa [zero_lt_iff, ne_zero_iff]

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 Γ'₀
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE

Tactic:
tfae_have 1 ↔ 2 := isEquiv_iff_val_lt_val

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y
⊢ [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1,
      ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v (-s) = 0

Tactic:
rwa [← Ideal.neg_mem_iff] at h

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✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ Infinite ι

Tactic:
refine (infinite_range_iff (Embedding.injective P.root)).mp (Infinite.mono ?_
    ((infinite_range_reflection_reflection_iterate_iff (P.coroot_root_two i)
    (P.coroot_root_two j) ?_).mpr ?_))
  · rw [range_subset_iff]
    intro n
    rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo (P.coroot_root_two i)
      (P.mapsTo_reflection_root i)).comp (bijOn_reflection_of_mapsTo (P.coroot_root_two j)
      (P.mapsTo_reflection_root j))).image_eq n]
    exact mem_image_of_mem _ (mem_range_self j)
  · rw [coroot_root_eq_pairing, coroot_root_eq_pairing, ← hc, mul_comm, coxeterWeight]
  · rw [LinearIndependent.pair_iff] at hl
    specialize hl (P.pairing j i) (-2)
    simp only [neg_smul, neg_eq_zero, two_ne_zero (α := R), and_false, imp_false] at hl
    rw [ne_eq, coroot_root_eq_pairing, ← sub_eq_zero, sub_eq_add_neg]
    exact hl

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp.left
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b
x : M₁
⊢ 0 ≤ Q₁ x

Tactic:
simpa only [add_zero, map_zero] using h x 0

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (-n • ⇑α + ⇑β) ≠ ⊥
⊢ n ≤ ↑(chainBotCoeff (⇑α) β)

Tactic:
by
  contrapose! hn
  lift n to ℕ using (Nat.cast_nonneg _).trans hn.le
  rw [Nat.cast_lt, ← @Nat.add_lt_add_iff_right (chainTopCoeff α β),
    chainBotCoeff_add_chainTopCoeff] at hn
  have := rootSpace_neg_nsmul_add_chainTop_of_lt α β hα hn
  rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ rootSpace H (- -n • ⇑α + ⇑β) ≠ ⊥

Tactic:
by rwa [neg_neg]

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

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
b : P.Base
⊢ span R (⇑P.root '' ↑b.support) = P.rootSpan R

Tactic:
← span_span_of_tower (R := ℤ),

Goal state after:
ι : 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
b : P.Base
⊢ span R ↑(span ℤ (⇑P.root '' ↑b.support)) = P.rootSpan R
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
hij' :
  P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = 2 ∨ P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4
aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
⊢ B.rootLength j < B.rootLength i

Tactic:
rcases aux₁ with hji | hji <;> rcases hij' with hij' | hij' | hij' | hij' | hij' | hij' <;>
  rw [hji, hij'] at aux₂ <;> lia

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

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
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root
⊢ ¬0 ≤ f ↔ f < 0

Tactic:
have := b.not_nonpos_iff_pos_of_sum_mem_range_root (-f) hf (by simpa)

Goal state after:
ι : 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
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root
this : ¬-f ≤ 0 ↔ 0 < -f
⊢ ¬0 ≤ f ↔ f < 0
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
⊢ baseOf (⇑P.root) f ⊆ baseOf (⇑P.coroot) g

Tactic:
refine fun i hi ↦ ⟨by obtain ⟨hi, -⟩ := hi; aesop, fun j hj k hk contra ↦ ?_⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
⊢ P.coroot j = 0 ∨ P.coroot k = 0