mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : ↑P.natDegree = (P.leadingCoeff • u • ↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P.leadingCoeff = head.leadingCoeff

Tactic:
head_degree_eq_natDegree

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : ↑P.natDegree = ↑head.natDegree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P.leadingCoeff = head.leadingCoeff
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: 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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : y ∈ H
this : x = y
⊢ End.IsSemisimple ↑((LieDerivation.ad K L) y)

Tactic:
hy

Goal state after:
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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : y ∈ H
this : x = y
⊢ End.IsSemisimple ↑S'
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: 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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : y ∈ H
⊢ S = ↑((LieDerivation.ad K L) y)

Tactic:
hy

Goal state after:
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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : y ∈ H
⊢ S = ↑S'
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 : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
y : M
⊢ y ∈ p → (reflection h) y ∈ p

Tactic:
hy

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ (reflection h) y ∈ p
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 : M
f : Dual R M
inst✝² : IsDomain R
inst✝¹ : NeZero 2
inst✝ : IsTorsionFree R M
h : f x = 2
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule ↑(reflection h)
y : M
hy : y ∈ p
hx : x ≠ 0
this : f y • x ∈ p
⊢ y ∈ LinearMap.ker f

Tactic:
have aux : f y • x ∈ p ⊓ R ∙ x := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
x : M
f : Dual R M
inst✝² : IsDomain R
inst✝¹ : NeZero 2
inst✝ : IsTorsionFree R M
h : f x = 2
p : Submodule R M
hp : Disjoint p (R ∙ x)
h' : p ∈ End.invtSubmodule ↑(reflection h)
y : M
hy : y ∈ p
hx : x ≠ 0
this : f y • x ∈ p
aux : f y • x ∈ p ⊓ R ∙ x
⊢ y ∈ LinearMap.ker f
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: 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
x : ↥H
h_mem : x ∈ corootSpace ⇑α
h_two : α x = 2
h₀ : ¬α.IsZero
⊢ x ∈ K ∙ coroot α

Tactic:
← coe_corootSpace_eq_span_singleton

Goal state after:
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
x : ↥H
h_mem : x ∈ corootSpace ⇑α
h_two : α x = 2
h₀ : ¬α.IsZero
⊢ x ∈ ↑(corootSpace ⇑α)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: 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α : ¬α.IsZero
⊢ IsCompl Weight.ker (K ∙ coroot α)

Tactic:
← coe_corootSpace_eq_span_singleton

Goal state after:
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α : ¬α.IsZero
⊢ IsCompl Weight.ker ↑(corootSpace ⇑α)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ eval (-1) (T R (↑n + 2)) = ↑↑(↑n + 2).negOnePow

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring

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

Goal state before:
pp: 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
hyp : coroot α = coroot β
hα : α.IsZero
⊢ β.IsZero

Tactic:
← coroot_eq_zero_iff

Goal state after:
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
hyp : coroot α = coroot β
hα : coroot α = 0
⊢ coroot β = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
      ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]

Tactic:
by
  let := b.isLieAbelian_cartan
  intro i
  fin_cases i
  · exact toLieSubmodule_le_rootSpace_zero R L H
  · exact b.borelLower_le_biSup
  · exact b.borelUpper_le_biSup

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

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R 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 : ↥H
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α
he_wt : ⁅↑h, e⁆ = α h • e
hf_wt : ⁅↑h, f⁆ = (-α) h • f
⊢ ↑(coroot α) ∈ H.toLieSubmodule

Tactic:
exact (coroot α).property

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 : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : AddCommGroup N₂
inst✝¹ : Module R N₂
inst✝ : P.IsRootSystem
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ span R (range ⇑(RootPairing.map e f g).coroot) = ⊤

Tactic:
by simp [Embedding.coe_trans, range_comp, RootPairing.map]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one (b' * (1 - Ideal.Quotient.mk (I ^ (n + 1)) c)) ?_

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ a * (b' * (1 - (mk (I ^ (n + 1))) c)) = 1
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ (mk (I ^ (n + 1))) (c * c) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ c * c ∈ I ^ (n + 1)
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
⊢ length S M = length R M

Tactic:
have : RingHomSurjective (algebraMap S R) := ⟨h⟩
  let f : M →ₛₗ[algebraMap S R] M := ⟨AddHom.id M, by simp⟩
  rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]

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
hv : v.Integers O
⊢ Nontrivial O ↔ Nontrivial R

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R

case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ Nontrivial O
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp.refine_2
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
y : Γ₀
⊢ y ∈ ⇑v ∘ ⇑(algebraMap O F) '' ↑I → y ≤ (⇑v ∘ ⇑(algebraMap O F)) x

Tactic:
hy

Goal state after:
case mp.refine_2
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
y : Γ₀
hy : y ∈ ⇑v ∘ ⇑(algebraMap O F) '' ↑I
⊢ y ≤ (⇑v ∘ ⇑(algebraMap O F)) x
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I ↔ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

Tactic:
constructor <;> intro h

Goal state after:
case mp.mp
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
h : b ∈ I
⊢ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

case mp.mpr
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
h : v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)
⊢ b ∈ I
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
⊢ y ∈ v.leSubmodule (v x) → y ∈ S

Tactic:
hy

Goal state after:
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)
⊢ y ∈ S
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 Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
y : ↥v.integer
⊢ y ∈ v.leIdeal (v ↑x) → y ∈ I

Tactic:
hy

Goal state after:
case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
y : ↥v.integer
hy : y ∈ v.leIdeal (v ↑x)
⊢ y ∈ I
Module: Mathlib.RingTheory.Valuation.ValuationRing

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

Tactic:
obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.left
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
⊢ Prime q

Tactic:
hpq

Goal state after:
case h.left
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
⊢ Prime p
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
hmn : m ≤ n
⊢ ↑x m = (Submodule.factor ⋯) (↑x n)

Tactic:
x.property hmn

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
hmn : m ≤ n
⊢ ↑x m = ↑x m
Module: Mathlib.RingTheory.Jacobson.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ ⊥.jacobson = ⊥

Tactic:
refine eq_bot_iff.2 fun f hf => ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
⊢ f ∈ ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case pos
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
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ under R (Ideal.map (algebraMap R S) I) = I

Tactic:
under_map_of_isPrime_disjoint (powers y) S hIm.isPrime

Goal state after:
case pos
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
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ I = I

case pos
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
J : Ideal S
h : J.IsMaximal
hJ✝ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ Disjoint ↑(powers y) ↑I
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ n • 1 = ↑n

Tactic:
nsmul_one

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ 1 x ≤ 1

Tactic:
one_apply_def

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ (if x = 0 then 0 else 1) ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ 1 x < 1 ↔ x = 0

Tactic:
one_apply_def

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ (if x = 0 then 0 else 1) < 1 ↔ x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b ↔ a ∣ b

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : (addVal R) a ≤ (addVal R) b
⊢ a ∣ b

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : a ∣ b
⊢ (addVal R) a ≤ (addVal R) b