mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

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 : ι
h2 : IsSMulRegular M 2
h : P.reflection i = P.reflection j
k : ι
⊢ P.root ((P.reflectionPerm i) k) = P.root ((P.reflectionPerm j) k)

Tactic:
simp [h]

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

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 : ι
h2 : IsSMulRegular M 2
⊢ P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩

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
i j : ι
h2 : IsSMulRegular M 2
h : P.reflectionPerm i = P.reflectionPerm j
⊢ P.reflection i = P.reflection j
Module: Mathlib.LinearAlgebra.RootSystem.Defs

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✝ : P.IsRootSystem
i j : ι
h : P.reflection i = P.reflection j
k : ι
⊢ P.root ((P.reflectionPerm i) k) = P.root ((P.reflectionPerm j) k)

Tactic:
simp [h]

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

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✝ : P.IsRootSystem
i j : ι
⊢ P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩

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
inst✝ : P.IsRootSystem
i j : ι
h : P.reflectionPerm i = P.reflectionPerm j
⊢ P.reflection i = P.reflection j
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
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
⊢ i = j

Tactic:
suffices ∀ k, c i (r k) = c j (r k) by
    rw [← EmbeddingLike.apply_eq_iff_eq r]
    exact eq_of_mapsTo_reflection_of_mem (f := c i) (g := c j) hfin (h_two i) (h_two j)
      (by rw [← this, h_two]) (by rw [this, h_two]) (h_mapsTo i) (h_mapsTo j) (mem_range_self j)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
⊢ ∀ (k : ι), (c i) (r k) = (c j) (r k)
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
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
hn : n ∈ span R ↑j.range
⊢ (p (i x)) n = 0

Tactic:
induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
⊢ (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 1

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 1 ^ 2) * eval 1 ((⇑derivative)^[k + 2] (U R n)) =
    (2 * ↑k + 3) * 1 * eval 1 ((⇑derivative)^[k + 1] (U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))
⊢ (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: 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 y : K
h : num A y * ↑(den A x) = num A x * ↑(den A y)
⊢ x = y

Tactic:
by simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h

Goal state after:
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: 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
h✝ : IsInteger A x
v : A
h : (algebraMap A K) v = x
⊢ IsUnit ↑(den A x)

Tactic:
apply IsRelPrime.isUnit_of_dvd (num_den_reduced A x).symm

Goal state after:
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
h✝ : IsInteger A x
v : A
h : (algebraMap A K) v = x
⊢ ↑(den A x) ∣ num A x
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
this : num A r ∣ (p.scaleRoots ↑(den A r)).coeff 0
⊢ num A r ∣ p.coeff 0

Tactic:
simp only [coeff_scaleRoots] at this
    have inst := Classical.propDecidable
    by_cases hr : num A r = 0
    · simp_all [nonZeroDivisors.coe_ne_zero]
    · refine dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this
      intro q dvd_num dvd_denom_pow hq
      apply hq.not_isUnit
      exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L j.range ∘ₗ j.rangeRestrict).range = ⊤

Tactic:
rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range j).span_range_inclusionSpan L

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ length R M = Order.height ⊤

Tactic:
apply WithBot.coe_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ↑(length R M) = ↑(Order.height ⊤)
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 = Order.coheight ⊥

Tactic:
apply WithBot.coe_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ↑(length R M) = ↑(Order.coheight ⊥)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ ↑↑s.length ≤ Order.krullDim (Submodule R M)

pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ Order.krullDim (Submodule R M) ≤ ↑↑s.length

Tactic:
· exact (Order.LTSeries.length_le_krullDim <| s.map ⟨id, fun h ↦ h.1⟩)

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
H : IsFiniteLength R M
this✝ : IsNoetherian R M
this : IsArtinian R M
⊢ Order.krullDim (Submodule R M) ≤ ↑↑s.length
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 : Submodule R M
⊢ length R ↥N = Order.height N

Tactic:
apply WithBot.coe_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ↑(length R ↥N) = ↑(Order.height N)
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 : Submodule R M
⊢ length R (M ⧸ N) = Order.coheight N

Tactic:
apply WithBot.coe_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ↑(length R (M ⧸ N)) = ↑(Order.coheight N)
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
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ Module.length R M = Module.length R N

Tactic:
apply WithBot.coe_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ ↑(Module.length R M) = ↑(Module.length R N)
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ IsNoetherianRing R

Tactic:
rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
    refine ⟨RelEmbedding.wellFounded ?_ h⟩
    have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
      fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1
    choose f hf using this
    exact
      { toFun := f
        inj' := fun x y e => by ext1; rw [hf, hf, e]
        map_rel_iff' := by
          dsimp
          intro a b
          rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
          rfl }

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

Goal state before:
pp: 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✝ : ValueGroup A K
a : K
ha : Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≠ 0
⊢ a ≠ 0

Tactic:
contrapose ha

Goal state after:
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✝ : ValueGroup A K
a : K
ha : a = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a = 0
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case 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
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g = 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
simp [h]

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

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝² : IsDomain 𝒪
this✝¹ : FaithfulSMul 𝒪 K
this✝ : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x * (algebraMap 𝒪 K) a = 1
⊢ x * (algebraMap 𝒪 K) ↑(1, ⟨a, ⋯⟩).2 = (algebraMap 𝒪 K) (1, ⟨a, ⋯⟩).1

Tactic:
by simpa using ha

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
n : ℕ
⊢ I ^ n • ⊤ ≤ (eval I M n).ker

Tactic:
by
  simp only [smul_le, mem_top, LinearMap.mem_ker, map_smul, coe_eval, forall_const]
  intro r r_in x
  rw [← Submodule.Quotient.mk_out (x.val n), ← Quotient.mk_smul, Quotient.mk_eq_zero]
  exact smul_mem_smul r_in mem_top

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

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

Tactic:
Finset.sum_insert has

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (f a + ∑ x ∈ s, f x) ≤ g
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g
⊢ v (∑ i ∈ insert a s, f i) < g

Tactic:
Finset.sum_insert has

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ i ∈ s✝, v (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g
hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g
⊢ v (f a + ∑ x ∈ s, f x) < g
Module: Mathlib.RingTheory.Valuation.Basic

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

Tactic:
map_sub_of_left_eq_zero v hx,

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ (addVal R) r = ↑n

Tactic:
by
  rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
      (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
    emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
    emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

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 x ≠ 0
H : ¬v (x + y) = 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) ⋯, ⋯⟩

pp: case pos
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) ⋯, ⋯⟩

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, ← 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]

Goal state after:
case pos
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) ⋯, ⋯⟩

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) ⋯, ⋯⟩
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
⊢ y * quotient x y + remainder x y = x

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
⊢ (y * quotient x y + if y ∣ x then 0 else x) = x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
Γ₀' : Type u_7
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
w : Valuation R Γ₀'
h : ∀ (r s : R), v r ≤ v s ↔ w r ≤ w s
⊢ ∀ (r s : R), v.restrict r ≤ v.restrict s ↔ w.restrict r ≤ w.restrict s

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ i, S i)) (↥(S i)) K
val✝ : K
hin : val✝ ∈ S i
hy : (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ = x
⊢ x ∈ S i

Tactic:
rwa [← hy]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False

Tactic:
let := h.toField

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
⊢ False
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝² x✝¹ : R
x✝ : x✝² ≈ x✝¹
⊢ ⟨span {x✝²}, ⋯⟩ = ⟨span {x✝¹}, ⋯⟩

Tactic:
simpa [span_singleton_eq_span_singleton]

Goal state after: