mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
⊢ Function.Surjective ⇑((LocalizedModule.map m.primeCompl) (LinearMap.lcomp R M (Submodule.subtype I)))

Tactic:
have eq'' : Iₘ.subtype.restrictScalars R = IsLocalizedModule.map m.primeCompl g h I.subtype :=
    IsLocalizedModule.ext m.primeCompl g (IsLocalizedModule.map_units h) (by ext; simp [g, h, Iₘ])

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
⊢ Function.Surjective ⇑((LocalizedModule.map m.primeCompl) (LinearMap.lcomp R M (Submodule.subtype I)))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
⊢ (ofPowerSeries ℤ S) (r • x) = r • (ofPowerSeries ℤ S) x

Tactic:
ext
  simp [coeff_coe, coeff_smul, smul_ite]

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

Goal state before:
pp: i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩

Tactic:
by
  rw [accumulate_apply]
  apply sum_eq_single_of_mem
  · rw [mem_filter]; exact ⟨mem_univ _, le_rfl⟩
  refine fun j hij hji ↦ ht j ?_
  rw [mem_filter_univ] at hij
  exact hmi.trans_le (hij.lt_of_ne (Fin.val_ne_iff.2 hji).symm).nat_succ_le

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}

Tactic:
apply coeff_eventually_equal (D := D) hℱ |>.mono

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := ⋯
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
⊢ ∀ (x : K⸨X⸩), (∀ d < D, coeff hℱ d = x.coeff d) → x ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ¬(sumSMulX c).totalDegree < 1

Tactic:
Nat.lt_one_iff,

Goal state after:
case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ¬(sumSMulX c).totalDegree = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V

Tactic:
have := (embedding γ.1)

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
this : WithZero (Multiplicative ℤ)
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)

Tactic:
refine ⟨le_succ_of_le h, ?_⟩

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 - 1 = k → ¬True ∧ True
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
S : Type u_4
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
⊢ (expand p hp).comp (substAlgHom hf) = substAlgHom ⋯

Tactic:
ext1 i
  simp [expand, subst_comp_subst_apply hf (HasSubst.X_pow hp)]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map ((RingHom.id (MvPolynomial (Fin (n + 1)) k)).comp ↑(T f)) I

Tactic:
id_comp,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map (↑(T f)) I
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n

Tactic:
| ind n H =>

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)

Tactic:
obtain ⟨r, hr⟩ : ∃ (a : O), a * (p : O) = (Ideal.Quotient.mk _ x).out - x :=
    Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _
  refine (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_ge ?_)
  rw [← map_sub, ← hr, hv.le_iff_dvd]
  exact fun hprx =>
    hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (wittPolynomial p ℤ n) = 1

Tactic:
by
  rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]
  · simp only [onePoly, one_pow, one_mul, map_pow, C_1, pow_zero, bind₁_X_right, if_true]
  · intro i _hi hi0
    simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
      bind₁_X_right, map_mul]
  · simp

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ (x✝¹ + y✝).coeff x✝ = peval (wittAdd p x✝) ![x✝¹.coeff, y✝.coeff]

Tactic:
exact add_coeff _ _ _

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (verschiebung (frobenius x)).coeff (n✝ + 1) = (x * ↑p).coeff (n✝ + 1)

Tactic:
rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

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

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ x ∈ RingHom.ker (truncate n) ↔ ∀ i < n, x.coeff i = 0

Tactic:
simp only [RingHom.mem_ker, truncate, RingHom.coe_mk, TruncatedWittVector.ext_iff,
    coeff_zero]
  exact Fin.forall_iff

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case inr.inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
hfg : (coeff (max m n + 1)) f * (coeff (max m n + 1)) g ≠ 0
⊢ ModP.preVal K v O p ((coeff (max m n + 1)) f * (coeff (max m n + 1)) g) ^ p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1)) g) ^ p ^ (max m n + 1)

Tactic:
ModP.preVal_mul hv hfg,

Goal state after:
case inr.inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
hfg : (coeff (max m n + 1)) f * (coeff (max m n + 1)) g ≠ 0
⊢ (ModP.preVal K v O p ((coeff (max m n + 1)) f) * ModP.preVal K v O p ((coeff (max m n + 1)) g)) ^ p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1)) g) ^ p ^ (max m n + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg.inl
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
h :
  ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k)) f)
⊢ ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ^ p ^ max (max m n) k ≤
    max (ModP.preVal K v O p ((coeff (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O p ((coeff (max (max m n) k)) g) ^ p ^ max (max m n) k)

Tactic:
exact le_max_of_le_left (pow_le_pow_left' h _)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).leadingCoeff = 1

Tactic:
← coeff_natDegree,

Goal state after:
n : ℕ
⊢ (hermite n).coeff (hermite n).natDegree = 1
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + k).choose k) -
      (↑k + 2) * ((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + (k + 2)).choose (k + 2)))

Tactic:
mul_comm (↑k + _ : ℤ),

Goal state after:
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + k).choose k) -
      (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + (k + 2)).choose (k + 2)) * (↑k + 2)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ.hc
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

pp: case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x

Tactic:
· apply Polynomial.differentiable_aeval

Goal state after:
case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
⊢ Irreducible f

Tactic:
let R' := R ⧸ nilradical R

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
R' : Type u_1 := R ⧸ nilradical R
⊢ Irreducible f
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -1 • f.toFun' S m + 1 • f.toFun' S m = 0

Tactic:
← _root_.add_smul

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (-1 + 1) • f.toFun' S m = 0
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ radical n ^ n

Tactic:
by
  grw [radical_eq_prod_primeFactors, ← dvd_prod_primeFactors_pow_self hn]

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Prime ↑p
dp : ↑p ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = ↑p

Tactic:
rw [← Nat.prime_iff_prime_int] at pp

Goal state after:
case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : ↑p ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = ↑p
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
inst✝ : Flat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsWeaklyRegular M rs
⊢ IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)

Tactic:
by
  induction rs generalizing M N with
  | nil => simp
  | cons x _ ih =>
    simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
    have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
    have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
    exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt.refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).degree = f.degree

Tactic:
H.degree_eq_coe_lift_order_map,

Goal state after:
case degree_lt.refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).degree = ↑(((map (IsLocalRing.residue A)) g).order.lift ⋯)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
⊢ map f S ≤ isotypicComponent R N ↥S

Tactic:
conv_lhs => rw [← S.range_subtype, ← LinearMap.range_comp]
  obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero
  · exact le_sSup ⟨.symm <| .ofInjective _ inj⟩
  · simp_rw [eq, LinearMap.range_zero, bot_le]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : ↑p ^ i = 0
⊢ i = n

Tactic:
by
  contrapose! hpi
  replace hin := lt_of_le_of_ne hin hpi; clear hpi
  have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
    rw [map_pow, map_natCast]
  rw [this, ne_eq, TruncatedWittVector.ext_iff, not_forall]; clear this
  use ⟨i, hin⟩
  rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]
  have : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
  exact one_ne_zero

Goal state after:
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
lift_lift

Goal state after:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{u + 1, max u (v + 1)} (lift.{v + 1, u} #α)

Tactic:
lift_lift

Goal state after:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃

Tactic:
← equiv_atom.1 h₁

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : atom a ~ l₃
⊢ atom a ~ l₃
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False

Tactic:
exact (opow_le_of_le_log he' (fst_le_log he)).not_gt h

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ upperBounds (f '' Iio a)

Tactic:
rintro _ ⟨b, hb, rfl⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
b : α
hb : b ∈ Iio a
⊢ f b ≤ f a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.repr < b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h; exact h₃

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : y ∈ ⋃₀ mk α A
a : (mk α A).Type
c : ((mk α A).Func a).Type
e : y.Equiv ((A a).Func c)
this : (A a).Func c ∈ mk (A a).Type (A a).Func
⊢ (A a).Func c ∈ A (?m.126 α A y x✝ a c e this)

Tactic:
rwa [eta] at this

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b o : ONote
⊢ Decidable (b.TopBelow o)

Tactic:
cases o <;> delta TopBelow <;> infer_instance

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ x✝.rank < (mk α✝ A✝).rank

Tactic:
rw [rank_congr h, ← succ_le_iff]
    apply Ordinal.le_iSup

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ range Γ_

Tactic:
by
  rw [(invVeblen₁_le o).lt_iff_ne, ne_eq, invVeblen₁_eq_iff, not_or]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: ⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) a

Tactic:
have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x := by
      refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
      rintro A ⟨z, rfl, hz⟩
      exact IH z hz

Goal state after:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) a