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

Goal state before:
pp: case refine_1.refine_3
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ y ∈ corootSpace ⇑α, H.subtype y = c₃ • h'

Tactic:
refine ⟨c₃ • coroot α, smul_mem _ _ <| by simp, ?_⟩

Goal state after:
case refine_1.refine_3
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ H.subtype (c₃ • coroot α) = c₃ • h'
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (S R n).comp (2 * X) = U R n

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℤ
t : R
ht : t = f y * g x - 2
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((m - 2) / 2)) *
              (Polynomial.eval t (S R ((m - 1) / 2)) + Polynomial.eval t (S R ((m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((m - 1) / 2)) *
            (Polynomial.eval t (S R (m / 2)) + Polynomial.eval t (S R ((m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z

Tactic:
simpa using reflection_mul_reflection_zpow_apply hf hg m z t ht

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 : ι
x : M
⊢ (P.reflection ((P.reflectionPerm j) i)) x = (P.reflection j * P.reflection i * P.reflection j) x

Tactic:
simp [reflection_apply, coreflection_apply]

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 : ι
x : M
⊢ x -
      ((P.toLinearMap x) (P.coroot i) - P.pairing j i * (P.toLinearMap x) (P.coroot j)) •
        (P.root i - P.pairing i j • P.root j) =
    x - (P.toLinearMap x) (P.coroot j) • P.root j -
        ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) • P.root i -
      ((P.toLinearMap x) (P.coroot j) - (P.toLinearMap x) (P.coroot j) * 2 -
          ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) * P.pairing i j) •
        P.root 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
i : ι
n : N
m : M
⊢ ((↑(P.reflection i).dualMap ∘ₗ P.flip) n) m = ((P.flip ∘ₗ ↑(P.coreflection i)) n) m

Tactic:
simp [map_sub, coreflection_apply, reflection_apply, mul_comm (P.toLinearMap m (P.coroot i))]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
this :
  Submodule.span ℕ ((fun m ↦ derivative (T R ↑m)) '' Set.Icc 0 (n - k)) ≤
    Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))
⊢ derivative ((⇑derivative)^[k] (T R ↑n)) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))

Tactic:
apply this
      convert! Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2
      simp [Set.image]

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 k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Tactic:
have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
    simp only [← coroot_reflectionPerm, hij]

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 k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
h : (P.coreflection i) (P.coroot k) = (P.coreflection j) (P.coroot k)
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case mem
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x u : M
hu : u ∈ ⇑P.root '' s
⊢ (P.reflection j) u = u

Tactic:
obtain ⟨i, his, rfl⟩ := hu

Goal state after:
case mem
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
i : ι
his : i ∈ s
⊢ (P.reflection j) (P.root i) = P.root i
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 : ι
inst✝¹ : NeZero 2
inst✝ : IsDomain R
this : IsReflexive R M
⊢ P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j

Tactic:
simp [coxeterWeight, IsOrthogonal, P.pairing_eq_zero_iff (i := i) (j := j)]

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

Goal state before:
pp: case right
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
⊢ num A r * inv ∣ p.coeff 0

Tactic:
have h : inv ∣ 1 := ⟨den A r, by simpa [mul_comm] using h_inv⟩

Goal state after:
case right
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
h : inv ∣ 1
⊢ num A r * inv ∣ p.coeff 0
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

pp: case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R

Tactic:
· intro H x y; infer_instance

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mpr.sup
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (N₁ N₂ : Submodule R R), N₁.FG → N₂.FG → N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal

Tactic:
rintro _ _ _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
      rw [← Submodule.span_insert]
      exact H _ _

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ v ((algebraMap O R) x)

Tactic:
← v.map_one,

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ v 1 ≤ v ((algebraMap O R) x)
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 y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ 1

Tactic:
← v.map_one,

Goal state after:
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 y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ v 1
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2

Tactic:
refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := H.total (Ideal.span {a}) (Ideal.span {b})
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm

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

Goal state before:
pp: case pos
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 : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : ¬a = 0
hb : b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
subst hb

Goal state after:
case pos
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 : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
ha : ¬a = 0
⊢ ∃ c, a * c = 0 ∨ 0 * c = a
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
inst✝ : IsAdicComplete I M
x : M
⊢ (ofLinearEquiv I M).symm ((of I M) x) = x

Tactic:
simp [ofLinearEquiv]

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
inst✝ : IsAdicComplete I M
x : AdicCompletion I M
⊢ (of I M) ((ofLinearEquiv I M).symm x) = x

Tactic:
simp [ofLinearEquiv]

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

Goal state before:
pp: case neg
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
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) ⊥.jacobson = ⊥

Tactic:
rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1
    ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)),
    comap_jacobson]

Goal state after:
case neg
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
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ sInf (comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}) ≤ ⊥.jacobson
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 : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x : M
⊢ Submodule.Quotient.mk ((lift I ha f ⋯) x) = (f n) x

Tactic:
simp only [lift, IsAdicComplete.lift, ofLinearEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply]

Goal state after:
R : Type u_1
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x : M
⊢ Submodule.Quotient.mk ((LinearEquiv.ofBijective (of I N) ⋯).symm ((AdicCompletion.lift I (extend ha f) ⋯) x)) =
    (f n) x
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ ↑0 ↔ ringKrullDim R ≤ 0 ∧ 0 ≤ ringKrullDim R

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 ↔ ringKrullDim R ≤ 0 ∧ 0 ≤ ringKrullDim R
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 : R
h : v x < 1
⊢ v (1 - x) = 1

Tactic:
← v.map_one,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Tactic:
obtain rfl | h := eq_or_ne x 0
  · simp
  · simp only [← one_lt_val_iff v h, le_or_gt]

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

Goal state before:
pp: case cons
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
⊢ ∃ n, Associated (x ^ n) (fa ::ₘ fs).prod

Tactic:
| cons fa fs fh =>

Goal state after:
case cons
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
⊢ ∃ n, Associated (x ^ n) (fa ::ₘ fs).prod
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
simp only [h, map_zero, zero_le, inv_zero, or_self]

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

Goal state before:
pp: case h.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
⊢ False

Tactic:
apply hs₂

Goal state after:
case h.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
⊢ s ∈ maximalIdeal R ^ Nat.find this
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ ∃ a ∈ maximalIdeal R, a ≠ 0

Tactic:
by_contra! h'

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ False
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 : R
⊢ quotient x 0 = 0

Tactic:
by simp [quotient]

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

Goal state before:
pp: 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 ∈ maximalIdeal R ^ n, b ∉ Ideal.span {a}

Tactic:
by_contra! h'

Goal state after:
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
h' : ∀ b ∈ maximalIdeal R ^ n, b ∈ Ideal.span {a}
⊢ False
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
hx0 : v x ≠ 0
hx1 : v x ≠ 1
⊢ Nontrivial Γ₀

Tactic:
exact ⟨v x, 1, hx1⟩

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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝⁷ : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝⁶ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝⁵ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁴ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝³ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝² : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝ : (ofClass w) (↑hy.choose).2 ≠ 0
⊢ (Units.mk0 ((ofClass w) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass w) (↑⋯.choose).2) ⋯ ≤
      (Units.mk0 ((ofClass w) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass w) (↑⋯.choose).2) ⋯ ↔
    (Units.mk0 ((ofClass v) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑⋯.choose).2) ⋯ ≤
      (Units.mk0 ((ofClass v) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑⋯.choose).2) ⋯

Tactic:
nth_rw 2 [mul_comm]

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✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝⁷ : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝⁶ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝⁵ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁴ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝³ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝² : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝ : (ofClass w) (↑hy.choose).2 ≠ 0
⊢ (Units.mk0 ((ofClass w) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass w) (↑⋯.choose).2) ⋯ ≤
      Units.mk0 ((ofClass w) (↑⋯.choose).2) ⋯ * (Units.mk0 ((ofClass w) (↑⋯.choose).1) ⋯)⁻¹ ↔
    (Units.mk0 ((ofClass v) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑⋯.choose).2) ⋯ ≤
      (Units.mk0 ((ofClass v) (↑⋯.choose).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑⋯.choose).2) ⋯
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: case inr
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
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))

Tactic:
apply Function.Injective.of_comp_right _
      (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective

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
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective
    (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) ∘ ⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ (algebraMap R (T ⧸ P)).IsIntegral

Tactic:
h_eq

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite

Tactic:
exact finite_of_finite_type_of_isJacobsonRing R S

Goal state after: