mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
⊢ (algebraMap K f.SplittingField) ↑q = ↑q.num / ↑q.den

Tactic:
rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map
            ((↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37)).comp
              (algebraMap k (MvPolynomial (Vars k) k)))
            ↑f -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
AlgHom.comp_algebraMap

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
⊢ (algebraMap k (AlgebraicClosure k)) ↑q = ↑q.num / ↑q.den

Tactic:
rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ n, (A ^ n).col i = 0

Tactic:
rw [← isNilpotent_transpose_iff, isNilpotent_iff_forall_row]
  simp_rw [← transpose_pow, row_transpose]

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
have := traceForm_eq_zero_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : traceForm R L ↥(shiftedGenWeightSpace R L M χ) = 0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainTopCoeff α β
⊢ genWeightSpace M (n • α + ⇑β) ≠ ⊥

Tactic:
by_cases hα : α = 0
  · rw [hα, smul_zero, zero_add]; exact β.genWeightSpace_ne_bot
  classical
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
  exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn

Goal state after:
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case succ
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hx : x ∈ ⊤.lcs L (k + 1)
hy : y ∈ LieSubmodule.ucs (k + 1) ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
LieSubmodule.ucs_succ,

Goal state after:
case succ
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ {x y : L}, x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((traceForm R L M) x) y = 0
x y : L
hx : x ∈ ⊤.lcs L (k + 1)
hy : y ∈ (LieSubmodule.ucs k ⊥).normalizer
⊢ ((traceForm R L M) x) y = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
m n : M
hB : ∀ (m : M), (B m) ((φ x) n) = -1 • (B ((φ x) m)) n
⊢ (-1) ^ k • -1 = (-1) ^ (k + 1)

Tactic:
rw [pow_succ (-1 : R), smul_eq_mul]

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

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

Tactic:
simp [C_sub_one, -C_neg, ih1, ih2]

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (-↑n)) = 2
ih2 : eval 2 (C R (-↑n + 1)) = 2
⊢ 2 * 2 - 2 = 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ S R (-1) = 0

Tactic:
by simpa using S_sub_one R 0

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

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

Tactic:
induction n with

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
α : M
hα : α ∈ range ⇑P.root
i : ι
⊢ P.reflection i • α ∈ range ⇑P.root

Tactic:
obtain ⟨j, rfl⟩ := hα

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 : ι
⊢ P.reflection i • P.root j ∈ range ⇑P.root
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
α : N
hα : α ∈ range ⇑P.coroot
i : ι
⊢ P.coreflection i • α ∈ range ⇑P.coroot

Tactic:
obtain ⟨j, rfl⟩ := hα

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 : ι
⊢ P.coreflection i • P.coroot j ∈ range ⇑P.coroot
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 : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
⊢ ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x

Tactic:
induction n with

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 + 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)

Tactic:
iterate_derivative_derivative_mul_X

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 + 1] (T R n) * X + k • (⇑derivative)^[k] (T R n) - ↑(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.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
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)

Tactic:
induction n with

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A.submatrix id ⇑e * B'.map ⇑K.subtype = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

Tactic:
← e.symm_symm,

Goal state after:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A.submatrix id ⇑e.symm.symm * B'.map ⇑K.subtype = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1
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 + 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)

Tactic:
iterate_derivative_derivative_mul_X

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 + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
      ↑((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: case mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n z : N
hz : z ∈ ↑j.range
⊢ (p (i x)) z = 0

Tactic:
obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
⊢ p (i x) = 0

Tactic:
ext n

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : ∀ (n : N), (p (i x)) n = 0
n : N
⊢ (p (i x)) n = 0 n
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) m = g

Tactic:
ext n

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ ((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) m) n = g n
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) b' * x

Tactic:
rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
⊢ (mk I M) f = 0

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n : ℕ
⊢ ↑((mk I M) f) n = ↑0 n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_2
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
⊢ (mk I M) ⟨a, ⋯⟩ = x

Tactic:
ext n

Goal state after:
case refine_2
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
n : ℕ
⊢ ↑((mk I M) ⟨a, ⋯⟩) n = ↑x n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Injective ⇑(of I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ (of I M) x = (of I M) 0

Tactic:
ext n

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Injective ⇑(of I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ ↑((of I M) x) n = ↑((of I M) 0) n
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: 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
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod x

Tactic:
use Multiset.replicate (Classical.choose (spec.2 hx)) p
    constructor
    · intro q hq
      have hpq := Multiset.eq_of_mem_replicate hq
      rw [hpq]
      refine ⟨spec.1.ne_zero, spec.1.not_isUnit, ?_⟩
      intro a b h
      by_cases ha : a = 0
      · rw [ha]
        simp only [true_or, dvd_zero]
      obtain ⟨m, u, rfl⟩ := spec.2 ha
      rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
      rw [Units.dvd_mul_right]
      by_cases hm : m = 0
      · simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h
      left
      obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
      rw [pow_succ']
      apply dvd_mul_of_dvd_left dvd_rfl _
    · rw [Multiset.prod_replicate]
      exact Classical.choose_spec (spec.2 hx)

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

Goal state before:
pp: 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

Tactic:
ext n

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 • ⊤]
n : ℕ
⊢ ↑((of I M) a) n = ↑u n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Surjective ⇑(of I M) ↔ IsPrecomplete I M

Tactic:
by
  constructor
  · refine fun h ↦ ⟨fun f hmn ↦ ?_⟩
    let u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), fun c ↦ (hmn c).symm⟩
    obtain ⟨x, hx⟩ := h u
    refine ⟨x, fun n ↦ ?_⟩
    simp only [SModEq]
    rw [← mkQ_apply _ x, ← eval_of, hx]
    simp [u]
  · intro h u
    choose x hx using (fun n ↦ Submodule.Quotient.mk_surjective (I ^ n • ⊤ : Submodule R M) (u.1 n))
    obtain ⟨a, ha⟩ := h.prec (f := x) (fun hmn ↦ by rw [SModEq, hx, ← u.2 hmn, ← hx]; simp)
    use a
    ext n
    simpa [SModEq, ← eval_of, ha, ← hx] using (ha n).symm

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ max (v x) (v (-y)) = max (v x) (v y)

Tactic:
rw [map_neg]

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})

pp: case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

pp: case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ 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:
case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
⊢ v₁ x < v₁ y ↔ v₂ x < v₂ y

Tactic:
← le_iff_le_iff_lt_iff_lt,

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
⊢ v₁ y ≤ v₁ x ↔ v₂ y ≤ v₂ x
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ f.coeff n ∈ comap C I

Tactic:
replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : ((mapRingHom i) f).coeff n = coeff 0 n
⊢ f.coeff n ∈ comap C I