mathlib-initiative/mathlib-tactics huggingface dataset:
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' : y ∈ H
hy : S = (ad K L) y
⊢ _root_.IsNilpotent ((ad K L) x - (ad K L) y)

Tactic:
hSN,

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' : y ∈ H
hy : S = (ad K L) y
⊢ _root_.IsNilpotent (N + S - (ad K L) y)
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
⊢ IsCompl Weight.ker (K ∙ coroot α)

Tactic:
by
  if hα : α.IsZero then
    simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker]
      using isCompl_top_bot
  else
    rw [← coe_corootSpace_eq_span_singleton]
    apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)
    replace hα : corootSpace α ≠ ⊥ := by simpa using hα
    rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα

Goal state after:
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 ι
i : ι
x : L
hx : x ∈ H
hx' : x ∈ Submodule.span R (range b.h)
⊢ (b.baseSupp i) ⟨x, hx⟩ • b.e i = ⁅x, b.e i⁆

Tactic:
induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]

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
h : (P.reflection i) (P.root k) = (P.reflection j) (P.root k)
⊢ P.pairing k i • P.root i = P.pairing k j • P.root j

Tactic:
simpa only [reflection_apply_root, sub_right_inj] using h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  ↑(n + 2) * U R (n + 2 - 1) =
    1 * T R (n + 1) + X * (↑(n + 1) * U R (n + 1 - 1)) -
      ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * derivative (U R n))
h₂ : T R (n + 1) = U R (n + 1) - X * U R (n + 1 - 1)
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)

Tactic:
linear_combination (norm := (push_cast; ring_nf))
    h₁ + (n + 2) * h₂

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

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

Tactic:
iterate_derivative_derivative_mul_X_sq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) -
      ((⇑derivative)^[k + 2] (T R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (T R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (T R n)) =
    (⇑derivative)^[k] (derivative (T R n) * X) - ↑(n ^ 2) * (⇑derivative)^[k] (T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
iterate_derivative_derivative_mul_X_sq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) -
      ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (U R n)) =
    ↑3 * (⇑derivative)^[k] (derivative (U R n) * X) - ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) :=
  AlgebraTensorModule.lift (restrictScalarsₗ R A (↥(span A ↑p)) (↥(span A ↑p)) A ∘ₗ lsmul A ↥(span A ↑p))
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := lTensor A (inclusionSpan A p)
hf : Injective ⇑f
hg : Injective ⇑g
this : ↑R (tensorToSpan A p) = ↑R f ∘ₗ g
⊢ Injective ⇑(tensorToSpan A p)

Tactic:
← LinearMap.coe_restrictScalars R,

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) :=
  AlgebraTensorModule.lift (restrictScalarsₗ R A (↥(span A ↑p)) (↥(span A ↑p)) A ∘ₗ lsmul A ↥(span A ↑p))
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := lTensor A (inclusionSpan A p)
hf : Injective ⇑f
hg : Injective ⇑g
this : ↑R (tensorToSpan A p) = ↑R f ∘ₗ g
⊢ Injective ⇑(↑R (tensorToSpan A p))
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Subsingleton R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

pp: case inr
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Nontrivial R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

Tactic:
· simp [Algebra.subsingleton R A]

Goal state after:
case inr
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Nontrivial R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case neg
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
j : ℕ
hj : j ≠ (p.scaleRoots ↑(den A r)).natDegree
h : (p.scaleRoots ↑(den A r)).natDegree ≤ j
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h hj.symm),
    zero_mul]

Goal state after:
case neg
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
j : ℕ
hj : j ≠ (p.scaleRoots ↑(den A r)).natDegree
h : (p.scaleRoots ↑(den A r)).natDegree ≤ j
⊢ ↑(den A r) ∣ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : f.ValueGroup₀
hxy : x < y
⊢ embedding x < embedding y

Tactic:
rw [← monoidWithZeroHom_strictMono.lt_iff_lt] at hxy

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : f.ValueGroup₀
hxy : (orderMonoidWithZeroHom f) x < (orderMonoidWithZeroHom f) y
⊢ embedding x < embedding y
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
⊢ length R M = length R N + length R P

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP

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 = ⊤
⊢ length R M = length R N + length R P
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 = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ length R M = length R N + length R P

Tactic:
← Module.length_compositionSeries s hs₁ hs₂,

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 = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ length R M = length R N + ↑s.length
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
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
⊢ ∀ {a b : { N // N.FG }}, DvdNotUnit ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b) ↔ b < a

Tactic:
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: case h
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) (c + 1) * (algebraMap A K) xa * (algebraMap A K) yb =
    (algebraMap A K) xa * (algebraMap A K) yb + (algebraMap A K) ya * (algebraMap A K) xb

Tactic:
simp only [← map_mul, ← map_add]

Goal state after:
case h
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ (algebraMap A K) ((c + 1) * xa * yb) = (algebraMap A K) (xa * yb + ya * xb)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) (c + 1) * (algebraMap A K) xb * (algebraMap A K) ya =
    (algebraMap A K) yb * (algebraMap A K) xa + (algebraMap A K) xb * (algebraMap A K) ya

Tactic:
simp only [← map_mul, ← map_add]

Goal state after:
case h
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
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ (algebraMap A K) ((c + 1) * xb * ya) = (algebraMap A K) (yb * xa + xb * ya)
Module: Mathlib.RingTheory.Valuation.ValuationRing

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

pp: case neg.inr
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 : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
      exact ⟨c, Or.inr e⟩

Goal state after:
case neg.inr
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 : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
I : Ideal R
M : Type u_4
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
N : Type u_5
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : SMul S R
inst✝⁵ : SMul T R
inst✝⁴ : SMul S M
inst✝³ : SMul T M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower T R M
inst✝ : SMulCommClass S T M
s : S
t : T
f : AdicCompletion I M
⊢ s • t • f = t • s • f

Tactic:
by ext; simp [val_smul, smul_comm]

Goal state after:
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
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : ↑x m ∈ I ^ n • ⊤
⊢ ((I ^ m • ⊤).liftQ ((I ^ n • ⊤).mkQ ∘ₗ LinearMap.id) ⋯) (↑x m) = 0

Tactic:
← LinearMap.mem_ker

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
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : ↑x m ∈ I ^ n • ⊤
⊢ ↑x m ∈ ((I ^ m • ⊤).liftQ ((I ^ n • ⊤).mkQ ∘ₗ LinearMap.id) ⋯).ker
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}

Tactic:
intro I
    rw [← Submodule.IsPrincipal.span_singleton_generator I]
    rintro ⟨I0, hI⟩
    apply span_singleton_eq_span_singleton.mpr
    apply h₂ _ hp
    rw [Ne, Submodule.span_singleton_eq_bot] at I0
    rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (a : R), C a ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intro r
    apply Subring.subset_closure
    apply Set.mem_insert_of_mem
    exact degree_C_le

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

Goal state before:
pp: case neg
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
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
have : x ≠ 0 := by
    rintro rfl
    apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
    simp [hx]

Goal state after:
case neg
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
⊢ ∃ n, I = maximalIdeal R ^ n
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

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

Tactic:
induction f using Multiset.induction with

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.DiscreteValuationRing.TFAE

Goal state before:
pp: case h
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
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x ^ (n + 1)) (fa ::ₘ fs).prod

Tactic:
rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]

Goal state after:
case h
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
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x * x ^ n) (fa * fs.prod)
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
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = ↑u * ϖ ^ n
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ↑n = span {↑u * ϖ ^ n}

Tactic:
span_singleton_mul_left_unit u.isUnit,

Goal state after:
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
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = ↑u * ϖ ^ n
⊢ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ↑n = span {ϖ ^ n}