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

Goal state before:
pp: case h
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
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * (((killingForm K L) e) f)⁻¹ * ((killingForm K L) e) f) • α' = coroot α

Tactic:
mul_assoc,

Goal state after:
case h
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
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * ((((killingForm K L) e) f)⁻¹ * ((killingForm K L) e) f)) • α' = coroot α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R ↑(n + 1)).degree

Tactic:
mul_assoc,

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * (X * U R ↑(n + 1))).degree
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h := T_eq_U_sub_X_mul_U (R := R) (-(n + 2))
  rw [T_neg, U_neg, Int.add_sub_cancel, ← neg_add' _ 1, U_neg,
    show n + 2 + 1 - 2 = n + 1 by ring] at h
  linear_combination (norm := ring_nf) 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 k : ι
hk : P.root k = P.root ((P.reflectionPerm i) j)
⊢ P.coroot k = (P.coreflection i) (P.coroot j)

Tactic:
EmbeddingLike.apply_eq_iff_eq

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 : ι
hk : k = (P.reflectionPerm i) j
⊢ P.coroot k = (P.coreflection i) (P.coroot 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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : ↑(u ^ n) = LinearMap.id
⊢ f = g

Tactic:
simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n

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
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
hab : (algebraMap A K) c' * (algebraMap A K) a' = (algebraMap A K) c' * (algebraMap A K) b' * x
⊢ (algebraMap A K) c' * (algebraMap A K) b' * mk' K a' ⟨b', b'_nonzero⟩ = (algebraMap A K) c' * (algebraMap A K) a'

Tactic:
mul_assoc,

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
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
hab : (algebraMap A K) c' * (algebraMap A K) a' = (algebraMap A K) c' * (algebraMap A K) b' * x
⊢ (algebraMap A K) c' * ((algebraMap A K) b' * mk' K a' ⟨b', b'_nonzero⟩) = (algebraMap A K) c' * (algebraMap A K) a'
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * (2 * ↑k + 1) * eval 1 ((⇑derivative)^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * ((2 * ↑k + 1) * eval 1 ((⇑derivative)^[k + 1] (T R n))) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ ((↑n ^ 2 - ↑k ^ 2) * ∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (↑n ^ 2 - ↑k ^ 2) * ((∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n))) =
    ∏ x ∈ insert k (Finset.range k), (↑n ^ 2 - ↑x ^ 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * ((2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n))) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
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
hx : x ≠ 0
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
have : Associated (num A x⁻¹⁻¹ : A) (den A x⁻¹) :=
    (associated_den_num_inv x⁻¹ (inv_ne_zero hx)).symm
  rw [inv_inv] at this
  exact this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * ∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * ((∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n))) =
    (∏ x ∈ insert k (Finset.range k), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: 𝔽 : Type u_3
inst✝¹ : Field 𝔽
inst✝ : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative)^[k] (T 𝔽 n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2)) / ↑(∏ l ∈ Finset.range k, (2 * l + 1))

Tactic:
eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),

Goal state after:
𝔽 : Type u_3
inst✝¹ : Field 𝔽
inst✝ : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative)^[k] (T 𝔽 n)) * ↑(∏ l ∈ Finset.range k, (2 * l + 1)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: 𝔽 : Type u_3
inst✝¹ : Field 𝔽
inst✝ : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative)^[k] (U 𝔽 n)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1) / ↑(∏ l ∈ Finset.range k, (2 * l + 3))

Tactic:
eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),

Goal state after:
𝔽 : Type u_3
inst✝¹ : Field 𝔽
inst✝ : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative)^[k] (U 𝔽 n)) * ↑(∏ l ∈ Finset.range k, (2 * l + 3)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case left
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
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * (algebraMap A K) inv * (algebraMap A K) ↑(den A r)

Tactic:
mul_assoc,

Goal state after:
case left
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
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * ((algebraMap A K) inv * (algebraMap A K) ↑(den A r))
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
⊢ length R M = length R N + length R P

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]

Tactic:
rw [Ideal.top_pow, top_smul]
    exact SModEq.top

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

Goal state before:
pp: case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
y : K
hy : y ∈ v.leSubmodule (v x)
this : v (y / x) ≤ 1
⊢ y ∈ S

Tactic:
simpa [Subring.smul_def, div_mul_cancel₀ _ hx0] using S.smul_mem ⟨_, this⟩ hx

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RPID : IsPrincipalIdealRing R
this : IsLocalRing R
P : Ideal R
right✝ : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hP1 : P ≠ ⊥
hP2 : P.IsPrime
hPM : P ≤ maximalIdeal R
⊢ maximalIdeal R ≠ ⊥

Tactic:
order

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * ↑u * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m * ↑u ∨ p ∣ b

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * (↑u * b)
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m * ↑u ∨ p ∣ b
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_1
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

Tactic:
obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x

Goal state after:
case refine_1.inl
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

case refine_1.inr
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
a : 𝒪
e : (algebraMap 𝒪 K) a = x⁻¹
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
⊢ (∃ f, Function.Surjective ⇑f) → IsJacobsonRing S

Tactic:
by
  rintro ⟨f, hf⟩
  rw [isJacobsonRing_iff_sInf_maximal]
  intro p hp
  use map f '' { J : Ideal R | comap f p ≤ J ∧ J.IsMaximal }
  use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm
  have : p = map f (comap f p).jacobson :=
    (IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm
  exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)

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

Goal state before:
pp: 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'
⊢ P'.jacobson ≤ P'

Tactic:
refine (IsLocalization.map_under (powers y) S P'.jacobson).ge.trans
    ((map_mono ?_).trans (IsLocalization.map_under (powers y) S P').le)

Goal state after:
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'
⊢ under R P'.jacobson ≤ under R P'
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:
rw [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:
rw [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.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsDomain R
h✝ : ¬IsField R
p : Ideal R
hp : p ≠ ⊥
h : p.IsPrime
⊢ False

Tactic:
exact hp.symm (Ideal.isPrime_bot.isMaximal'.eq_of_le h.ne_top bot_le)

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
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ((addVal R) x) = span {x}

Tactic:
· obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
      obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx0 hϖ
      rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_natCast, hϖ.maximalIdeal_eq, span_singleton_pow]

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:
mul_assoc,

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).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) ⋯
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : I = ⊥
⊢ I ≤ J ∨ J ≤ I

Tactic:
order

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
hJ : J = ⊥
⊢ I ≤ J ∨ J ≤ I

Tactic:
order

Goal state after: