mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
⊢ (∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)) → B.IsSymm

Tactic:
by
    refine fun h ↦ ⟨fun x y ↦ ?_⟩
    obtain ⟨fx, tx, ix, -, hx⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : x ∈ Submodule.span R (Set.range b))
    obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))
    rw [← hx, ← hy]
    simp only [map_sum, map_smul, coe_sum, Finset.sum_apply, smul_apply, smul_eq_mul,
      Finset.mul_sum]
    rw [Finset.sum_comm]
    refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)
    rw [mul_left_comm]
    obtain ⟨i, rfl⟩ := ix h₁
    obtain ⟨j, rfl⟩ := iy h₂
    rw [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
⊢ IsLieAbelian ↥H

Tactic:
rw [b.cartan_eq_lieSpan, isLieAbelian_lieSpan_iff]

Goal state after:
ι : 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
⊢ ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)

Tactic:
rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl,
      ← orthogonal_toSubmodule _ hΦ_inv, LieSubmodule.disjoint_toSubmodule]
  exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ∃ T ⊆ S, t.sup id = sSup T

Tactic:
refine ⟨t, ?_, Finset.sup_id_eq_sSup t⟩

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ↑t ⊆ S
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
⊢ x ∈ W ⊓ ker B

Tactic:
rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩

Goal state after:
case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ W
hker : ⟨x, hx⟩ ∈ ↑(domRestrict B W).ker
⊢ (Submodule.subtype W) ⟨x, hx⟩ ∈ W ⊓ ker B
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
⊢ ((toMatrix snf.bN snf.bN) (f.restrict hf')).trace = ((toMatrix snf.bM snf.bM) f).trace

Tactic:
set A : Matrix (Fin n) (Fin n) R := toMatrix snf.bN snf.bN (f.restrict hf')

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
⊢ A.trace = ((toMatrix snf.bM snf.bM) f).trace
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
x : L
hx : x ∈ ⊤
⊢ x ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
replace hx : x ∈ lieSpan R L (range b.e ∪ range b.f) := by simp [b.span_ef]

Goal state after:
ι : 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
x : L
hx : x ∈ lieSpan R L (range b.e ∪ range b.f)
⊢ x ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
P : R[X]
hP : P ∈ ↑S '' Set.Iio m
⊢ P ∈ ↑(degreeLT R m)

Tactic:
obtain ⟨i, hi, rfl⟩ := (Set.mem_image _ _ _).mp hP

Goal state after:
case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : ↑S i ∈ ↑S '' Set.Iio m
⊢ ↑S i ∈ ↑(degreeLT R m)
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
⊢ Bijective fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩

Tactic:
by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ C R 0 = 2

Tactic:
by simp [C]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ C R 1 = X

Tactic:
by simp [C]

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 α) ∈ rootSpace H 0

Tactic:
rootSpace_zero_eq K L H

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (C R n) = eval x (C R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_C]

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 : ι
inst✝¹ : NeZero 2
inst✝ : IsDomain R
⊢ i ≠ -i

Tactic:
have := Module.IsReflexive.of_isPerfPair P.toLinearMap

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 : ι
inst✝¹ : NeZero 2
inst✝ : IsDomain R
this : IsReflexive R M
⊢ i ≠ -i
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
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
f : ↥H → R
hf : f ∈ sU
hg : f ∈ sV
⊢ ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)

Tactic:
simpa [hsU] using hf

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) - (⇑derivative)^[k] (↑(n ^ 2) * 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_intCast_mul,

Goal state after:
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)
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) - (⇑derivative)^[k] (↑((n + 2) * n) * 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_intCast_mul,

Goal state after:
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)
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this : IsReflexive L M
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
have : IsReflexive L N := .of_isPerfPair p.flip

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝ : IsReflexive L M
this : IsReflexive L N
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)
Module: Mathlib.RingTheory.DedekindDomain.Basic

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : IsLocalRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Module.Finite R A
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
⊢ (p.primesOver A).Nonempty

Tactic:
obtain ⟨w', hmax, hover⟩ := exists_maximal_ideal_liesOver_of_isIntegral (S := A) p
    exact ⟨w', hmax.isPrime, hover⟩

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

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

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

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

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (-↑k) = T R (m + -↑k) + T R (m - -↑k)
ih2 : 2 * T R m * T R (-↑k + 1) = T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))
⊢ 2 * T R m * T R (-↑k - 1) = T R (m + (-↑k - 1)) + T R (m - (-↑k - 1))

Tactic:
have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
I J K : Ideal R
inst✝¹ : J.IsTwoSided
inst✝ : K.IsTwoSided
hIJ : J ≤ I
hJK : K ≤ J
x : R ⧸ K
h : x ∈ map (mk K) I
⊢ x ∈ comap (factor hJK) (map (mk J) I)

Tactic:
rcases mem_image_of_mem_map_of_surjective (mk K) Quotient.mk_surjective h with ⟨r, hr, eq⟩
    simpa only [← eq] using! mem_map_of_mem (mk J) hr

Goal state after:
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:
← monoidWithZeroHom_strictMono.lt_iff_lt

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.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
a : f.ValueGroup₀
ha : 0 < a
b c : f.ValueGroup₀
hbc : b < c
⊢ a * b < a * c

Tactic:
simp only [← (embedding_strictMono (f := f)).lt_iff_lt, map_mul] at *
    exact (mul_lt_mul_iff_of_pos_left ha).mpr hbc

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r x : ↥v.integer
h : x ∈ ((v.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ ↑(r • x) ∈ v.leAddSubgroup γ

Tactic:
simpa using mul_le_of_le_one_of_le r.prop h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q

Tactic:
rcases hR with ⟨ϖ, hϖ, hR⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
⊢ Associated p q
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}
x y : R
e' : x * (a * g) + y * (b * g) = g
⊢ a * g ∣ b * g ∨ b * g ∣ a * g

Tactic:
rcases eq_or_ne g 0 with h | h

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

case 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
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ a * g ∣ b * g ∨ b * g ∣ a * g
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 := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
⊢ ∀ b ∈ Multiset.replicate (Classical.choose ⋯) p, Prime b

Tactic:
intro q hq

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
⊢ Prime q
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 5 := iff_local_bezout_domain

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2
tfae_1_iff_5 : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
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 * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Tactic:
simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h

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

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

Tactic:
refine ⟨⟨0, 1⟩, by simpa [h0, eq_comm] using ha⟩

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD I ^ n • ⊤]
⊢ ∃ a, (of I M) a = u

Tactic:
use a

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD I ^ n • ⊤]
⊢ (of I M) a = u
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 ≤ J

Tactic:
refine Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)

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
⊢ J.jacobson = J