mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
⊢ t ∈ powersetCard (i + 1) univ →
    t ≠ Iic ⟨i, him⟩ →
      supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
        supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)

Tactic:
ht

Goal state after:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
⊢ t ≠ Iic ⟨i, him⟩ →
    supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
      supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hdi
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (ι a) (Sum.inl a) = 1

Tactic:
simp [ι]

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

Tactic:
rw [pairMap_of_snd_notMem_fst σ h1]
    simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]
    nth_rewrite 2 [← pow_one (X t.snd)]
    simp only [← pow_add, ← Nat.add_sub_assoc (Nat.lt_of_le_of_ne h.left (mt h.right h1)), add_comm,
      Nat.succ_eq_add_one, Nat.add_sub_add_right]
    rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]
    simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : (if m = p • d then 1 else 0) ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
hc : ¬m = p • d
⊢ False

Tactic:
if_neg hc

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : 0 ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
hc : ¬m = p • d
⊢ False
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0

Tactic:
rw [sum_eq_zero]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
by
  induction n using Nat.strongRecOn with | ind n IH => ?_
  rw [xInTermsOfW_eq, mul_comm, map_mul, map_sub, map_sum, constantCoeff_C,
    constantCoeff_X, zero_sub, mul_neg, neg_eq_zero, sum_eq_zero, mul_zero]
  intro m H
  rw [mem_range] at H
  simp only [map_mul, map_pow, map_natCast, IH m H]
  rw [zero_pow, mul_zero]
  exact pow_ne_zero _ hp.1.ne_zero

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ 0, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
    rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab
    by_contra ne
    have eq := eq_C_of_isEmpty (a - b)
    have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne ne <| map_zero _
    obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit
    have one : c • (a - b) = 1 := by
      rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
    exact hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittOne, wittStructureRat, map_zero, map_one, map_wittStructureInt]
  induction n using Nat.strong_induction_on with | h n IH => ?_
  rw [xInTermsOfW_eq]
  simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right,
    bind₁_C_right]
  rw [sub_mul, one_mul]
  rw [Finset.sum_eq_single 0]
  · simp only [one_mul, pow_zero]
    simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
  · intro i hin hi0
    rw [Finset.mem_range] at hin
    rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]
  · grind

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (-x).ghostFun = -x.ghostFun

Tactic:
by ghost_fun_tac -X 0, ![x.coeff]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0

Tactic:
intro h
  simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R

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

Goal state before:

Tactic:
aeval (fun k => x.coeff k) (frobeniusPoly p n) =
        aeval (fun k => x.coeff k)
          (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) := ?_
    _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
    _ = x.coeff n ^ p := ?_

Goal state after:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) (frobeniusPoly p n) =
    (aeval fun k ↦ x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))

case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    (aeval fun k ↦ x.coeff k) (X n ^ p)

case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) (X n ^ p) = x.coeff n ^ p
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 = 1

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Goal state after:
case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (i : ℕ), liftFun f 1 - 1 ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ * y✝) = liftFun f x✝ * liftFun f y✝

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Goal state after:
case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ ∀ (i : ℕ), liftFun f (x✝ * y✝) - liftFun f x✝ * liftFun f y✝ ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 = 0

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Goal state after:
case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (i : ℕ), liftFun f 0 - 0 ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_4
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ + y✝) = liftFun f x✝ + liftFun f y✝

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Goal state after:
case refine_4
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ ∀ (i : ℕ), liftFun f (x✝ + y✝) - (liftFun f x✝ + liftFun f y✝) ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ (lift f f_compat) x = g x

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Goal state after:
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ ∀ (i : ℕ), (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
⊢ x.coeff i =
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i + (Finset.Iic n \ {i}).sum g

pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
⊢ ∀ x_1 ∈ Finset.Iic n \ {i},
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i = g x_1

Tactic:
· simp [g]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
⊢ ∀ x_1 ∈ Finset.Iic n \ {i},
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i = g x_1
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: case hg
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this✝ : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
this : ⇑(Ideal.Quotient.mk 𝔭) ∘ ⇑(fontaineTheta R p) = (fun x ↦ (PreTilt.coeff 0) x) ∘ fun x ↦ x.coeff 0
⊢ Function.Surjective fun x ↦ (PreTilt.coeff 0) x

Tactic:
exact Perfection.coeff_surjective hF 0

Goal state after:
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:
rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]

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.HilbertPoly

Goal state before:
pp: case p1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
this : (fun x a ↦ a) = fun x a ↦ a * 1 ^ x
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
        | 0 => 0
        | d.succ =>
          ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
            (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).coeff
      (d - rootMultiplicity 1 p - 1) ≠
    0

Tactic:
simp only [finsetSum_coeff, coeff_smul, smul_eq_mul, coeff_preHilbertPoly_self,
      ← Finset.sum_mul, ← sum_def _ (fun _ a => a), this, ← eval_eq_sum, eval_mul, eval_pow,
      eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq,
      false_and, or_false, inv_eq_zero, cast_eq_zero, not_or]

Goal state after:
case p1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
this : (fun x a ↦ a) = fun x a ↦ a * 1 ^ x
⊢ ¬eval 1 q = 0 ∧ ¬(d - rootMultiplicity 1 p - 1)! = 0
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (log A) = log A'

Tactic:
by
  ext n; simp only [coeff_map, coeff_log]; split_ifs <;> simp [RingHom.map_rat_algebraMap]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : Nontrivial A
i : ℕ
hi : i < 1
⊢ (coeff i) (log A) = 0

Tactic:
by simp [Nat.lt_one_iff.mp hi]

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
m : M
⊢ id.ground m = m

Tactic:
rw [ground_id, id_eq]

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
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ₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N (((h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ)).comp (mkₐ R (RingCon.ker ↑φ))).toLinearMap)
      (f.toFun' A p) =
    (rTensor N (ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp (mkₐ R (RingCon.ker ↑ψ)))).toLinearMap)
      (f.toFun' B q)

Tactic:
ht

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ₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N ((ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)).comp (mkₐ R (RingCon.ker ↑φ))).toLinearMap)
      (f.toFun' A p) =
    (rTensor N (ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp (mkₐ R (RingCon.ker ↑ψ)))).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
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤

Tactic:
have := ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
    rw [Subsingleton.elim f 0, Subsingleton.elim (H.div 0) 0, Subsingleton.elim (H.mod 0) 0]
    exact g.isWeierstrassDivisionAt_zero _

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
⊢ ∀ (p : Ideal R') [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)

Tactic:
intro p hp

Goal state after:
R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
⊢ ∀ (p : Ideal R) [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)

Tactic:
intro p hp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i : ℕ
⊢ (coeff i) q ∈ I ^ (k + 1)

Tactic:
rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i : ℕ
⊢ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat))
      (↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)) ∈
    I ^ (k + 1)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥a], Nonempty (↥(Submodule.map N.subtype a) ≃ₗ[R] S)

Tactic:
exact forall₂_congr fun m _ ↦ ⟨fun ⟨e'⟩ ↦ ⟨(e m).symm.trans e'⟩, fun ⟨e'⟩ ↦ ⟨(e m).trans e'⟩⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S✝ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S✝
inst✝³ : Module R M
inst✝² : Module R S✝
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
h : IsIsotypicOfType R M S✝
n : ℕ
S : Fin n → Submodule R M
e : M ≃ₗ[R] Π₀ (i : Fin n), ↥(S i)
hs : ∀ (i : Fin n), IsSimpleModule R ↥(S i)
⊢ ∃ n, Nonempty (M ≃ₗ[R] Fin n → S✝)

Tactic:
exact ⟨n, ⟨e.trans (DFinsupp.mapRange.linearEquiv fun i ↦ (h (S i)).some)
    |>.trans (finsuppLequivDFinsupp R).symm |>.trans (Finsupp.linearEquivFunOnFinite ..)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ Submodule.map p S.subtype.range

Tactic:
← LinearMap.range_comp,

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ (p ∘ₗ S.subtype).range
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ moebius a = moebius b

Tactic:
rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]

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

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Tactic:
· rw [Ideal.map_le_iff_le_comap]
    intro x hx
    exact hx

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq''' : q' ≠ 0
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0

Tactic:
simpa only [Ne, map_zero] using
      (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''

Goal state after: