mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.map (algebraMap S T) (Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
⊢ Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd) = ⊤

Tactic:
Ideal.map_span

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
⊢ Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd) = ⊤
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝² : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun (m • x) =
      ↑(IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv m •
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun x

Tactic:
· intro r m
    obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r
    apply ((Module.End.isUnit_iff _).mp
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1
    dsimp
    simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ ↑x ∈ ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))

Tactic:
SetLike.mem_coe,

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ ↑x ∈ Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ (idealX K).intValuation ↑Polynomial.X = exp (-1)

Tactic:
← intValuation_eq_of_coe

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ (Polynomial.idealX K).intValuation Polynomial.X = exp (-1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
⊢ f.coeff n = 0

Tactic:
set F := powerSeriesPart f with hF

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
⊢ f.coeff n = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
⊢ f.coeff n = 0

Tactic:
· obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))
    obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (a := n - s) (by grind)
    obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by lia)
    rw [sub_eq_iff_eq_add.mp hm, add_comm, ← neg_neg (s : ℤ), ← hs, neg_neg,
      ← powerSeriesPart_coeff]
    apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
    rw [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg,
      exp_add, valuation_single_zpow, neg_neg]
    gcongr

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D) * (exp ↑s)⁻¹

pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ 0 < exp ↑s

Tactic:
exp_neg,

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ (exp D)⁻¹ * (exp ↑s)⁻¹

case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ 0 < exp ↑s
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : m i = 0
⊢ IsWeightedHomogeneous w 0 n'

Tactic:
apply isWeightedHomogeneous_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_2
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w 0 n'

Tactic:
apply isWeightedHomogeneous_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}

Tactic:
rw [mem_filter]

Goal state after:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ univ ∧ ↑⟨i, ⋯⟩ ≤ ↑⟨i, hin⟩
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t

Tactic:
split_ifs with h1 h2 h3

Goal state after:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1
⊢ (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t

case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1
⊢ ((cons t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case right.inr
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with | _ t ih

Goal state after:
case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
t : Lex (Fin n →₀ ℕ)
ih :
  ∀ y < t,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
he : supDegree (⇑toLex) p = t
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ {x ∈ pairs σ k |
      match x with
      | (s, snd) => #s < k} =
    (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ

Tactic:
ext; aesop (add unsafe le_of_lt)

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
i✝ j✝ : ι
⊢ ((diagonal fun x ↦ r) * single i i 1) i✝ j✝ = (single i i 1 * diagonal fun x ↦ r) i✝ j✝

Tactic:
simp [Matrix.single]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
have not_le : ¬ p • m ≤ p • n := by
        obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)
        have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]
        exact Not.intro fun a ↦ this (a i)
      rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg h_le]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
x : M × M
hx : x ∈ antidiagonal a
⊢ ‖f x.1 * g x.2‖ * C a ≤ ‖f x.1‖ * C x.1 * (‖g x.2‖ * C x.2)

Tactic:
grw [mul_mul_mul_comm, ← hC, Finset.mem_antidiagonal.mp hx, ← norm_mul_le]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ Valued.v f ≤ 1

Tactic:
← valuation_compare (K := K) f,

Goal state after:
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ Valued.v ((LaurentSeriesRingEquiv K) f) ≤ 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0

Tactic:
Finsupp.single_eq_zero

Goal state after:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ (ghostComponent n) x

Tactic:
rw [WittVector.ghostComponent_apply, wittPolynomial, MvPolynomial.aeval_sum]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ ∑ i ∈ Finset.range (n + 1), (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k.succ)) f = 0
⊢ (coeff R p (n + k)) f = 0

Tactic:
rw [Nat.add_succ] at h
    rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ (Perfection.lift p R S) (π.comp f) = (↑m.equiv).comp f

Tactic:
by rw [← Equiv.eq_symm_apply]; rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih : (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ (bind₁ (Function.uncurry ![wittMulN p n, X])) ((bind₁ (wittStructureInt p (X 0 + X 1))) (wittPolynomial p ℤ k)) =
    ↑(n + 1) * wittPolynomial p ℤ k

Tactic:
wittStructureInt_prop

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih : (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ (bind₁ (Function.uncurry ![wittMulN p n, X]))
      ((bind₁ fun i ↦ (rename (Prod.mk i)) (wittPolynomial p ℤ k)) (X 0 + X 1)) =
    ↑(n + 1) * wittPolynomial p ℤ k
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n k : ℕ
⊢ ((⇑verschiebung)^[n] x).coeff (k + n) = x.coeff k

Tactic:
by
  induction n with
  | zero => simp
  | succ k ih => rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih

Goal state after:
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
by
  refine map_injective (MvPolynomial.map (Int.castRingHom ℚ))
    (MvPolynomial.map_injective _ Int.cast_injective) ?_
  simp only [teichmuller_mul_aux₁, map_teichmullerFun, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
x : 𝕎 R♭
⊢ (factorPowSucc 𝔭 (n + 1)) ((fontaineThetaModPPow R p (n + 1)) x) = (fontaineThetaModPPow R p n) x

Tactic:
by
  simp [← factorPowSucc_comp_fontaineThetaModPPow n]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).leadingCoeff = (↑d !)⁻¹

Tactic:
rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) = ↑((n - k + d).choose d)

Tactic:
ascPochhammer_nat_eq_natCast_ascFactorial

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * ↑((n - k + 1).ascFactorial d) = ↑((n - k + d).choose d)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)

Tactic:
let θ := (quotientKerEquivRangeₐ (R := R) ψ).symm.toAlgHom.comp
    (h'.comp (quotientKerEquivRangeₐ φ).toAlgHom)

Goal state after:
R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g 0 (H.mod 0) ⊤

Tactic:
Subsingleton.elim (H.mod 0) 0

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g 0 0 ⊤
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ IsRegularLocalRing R ↔ ↑(Module.finrank (ResidueField R) (CotangentSpace R)) = ringKrullDim R

Tactic:
rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (rTensor M ψ.toLinearMap) p = t ∧ ψ q = s

Tactic:
by
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec

Goal state after: