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

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i ∈ range n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))

Tactic:
rw [mem_range] at h

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
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
i : ℕ
hi : i < n + 1
⊢ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
simp [MvPolynomial.aeval_monomial, map_pow]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x

Tactic:
obtain ⟨ψ, hg⟩ := hg

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)

Tactic:
by
  apply pow_dvd_of_le_emultiplicity
  rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]

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
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
⊢ IsPoly p fun R _Rcr ↦ g ∘ f

Tactic:
obtain ⟨ψ, hg⟩ := hg

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ IsPoly p fun R _Rcr ↦ g ∘ f
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p * X (n + 1) -
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          (∑ i ∈ range n,
            ∑ j ∈ range (p ^ (n - i)),
              (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
sub_eq_add_neg,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p * X (n + 1) +
      -(C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            (∑ i ∈ range n,
              ∑ j ∈ range (p ^ (n - i)),
                (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                  C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ h (f x_1) (g y)

Tactic:
obtain ⟨ψ, hg⟩ := hg

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ h (f x_1) (g y)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)

Tactic:
· rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
      add_tsub_cancel_right]

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
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ g (f x_1 y)

Tactic:
obtain ⟨ψ, hg⟩ := hg

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ g (f x_1 y)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly₂ p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
obtain ⟨ψ, hg⟩ := hg

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : v ↑p = 0
⊢ 0 ≤ 0 ^ (1 / ↑p) * 0 ^ (1 / ↑p)

Tactic:
exact zero_le

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

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

pp: 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)

pp: 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

Tactic:
· conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl

Goal state after:
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.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0

Tactic:
change (1 : ModP O p) ≠ 0

Goal state after:
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
⊢ 1 ≠ 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ X m ^ p ^ (n - m) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)

Tactic:
if_neg <| not_not_intro Pm,

Goal state after:
case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ X m ^ p ^ (n - m) + 0 ^ p ^ (n - m) = X m ^ p ^ (n - m)
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0

Tactic:
by
  simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]
  refine ⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩
  · rw [hu, mul_charP_coeff_zero]
  · use (frobeniusEquiv p k).symm (x.shift 1)
    calc
    _ = verschiebung (x.shift 1) := by
      simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
    _ = _ := by
      rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
          RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
⊢ ∀ i < g.natDegree, (PowerSeries.coeff i) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = 0

Tactic:
· intro i hi
    simp [mapf, PowerSeries.coeff_X_pow_mul', hi]

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0

Tactic:
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
    rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑(p * (1 - X)) * ↑(invOneSubPow F (d + 1))) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
coeff_mul_invOneSubPow_eq_hilbertPoly_eval (d + 1) hn

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a
n : ℕ
⊢ (X - X ^ 2) ^ n = ∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)

Tactic:
sub_eq_add_neg,

Goal state after:
case e_a
n : ℕ
⊢ (X + -X ^ 2) ^ n = ∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * (↑n ! * shiftedLegendre n).comp (1 - X) = ↑n ! * shiftedLegendre n

Tactic:
factorial_mul_shiftedLegendre_eq,

Goal state after:
n : ℕ
⊢ (-1) ^ n * ((⇑derivative)^[n] (X ^ n * (1 - X) ^ n)).comp (1 - X) = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t =
    (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'

Tactic:
obtain ⟨Q, hPQ, h⟩ := Module.DirectLimit.exists_eq_of_of_eq h

Goal state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t =
    (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t'
Q : { P // P.FG }
hPQ : ⟨P, hP⟩ ≤ Q
h : (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'
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 φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)

Tactic:
rw [← φ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ φ,
    ← ψ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ ψ,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc _, 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: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f k) ∈ I ^ k

Tactic:
induction k generalizing hi i with
  | zero => simp
  | succ k hq =>
    rw [seq]
    set q := H.seq f k
    set s := f - g * q
    set n := (g.map (Ideal.Quotient.mk I)).order.toNat
    have hs := s.eq_X_pow_mul_shift_add_trunc n
    set s₀ := s.trunc n
    set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
    set q' := q + s₁ * H.isUnit_shift.unit⁻¹
    have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ := by
      trans s + g * (q - q')
      · simp_rw [s]; ring
      simp_rw [q']
      rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
      nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
      rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
      ring
    rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      pow_succ']
    refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i
    rw [coeff_mk]
    exact hq (by simp)

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n

Tactic:
simpa using hx

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

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1))) * (rename (Prod.mk 0)) (X (n + 1))

Tactic:
rename_C,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    C (↑p ^ (n + 1)) * (rename (Prod.mk 0)) (X (n + 1))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1))) * (rename (Prod.mk 1)) (X (n + 1))

Tactic:
rename_C,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    C (↑p ^ (n + 1)) * (rename (Prod.mk 1)) (X (n + 1))
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b ≠ 0

Tactic:
simpa only [map_zero] using
      (IsFractionRing.injective (WittVector p k) (FractionRing (WittVector p k))).ne
        (frobeniusRotation_nonzero p hr' hq')

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n

Tactic:
exact mul_polyOfInterest_aux3 _ _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
⊢ EventuallyConst f atTop

Tactic:
eventuallyConst_atTop

Goal state after:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case inr
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
let o₃ := o₂ - o₁

Goal state after:
case inr
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝²] {a}

Tactic:
by
  obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 ha
  by_cases ha' : IsMax a
  · convert! isOpen_Ioi (a := b) using 1
    rw [hb.Ioi_eq]
    grind [IsMax]
  · convert! isOpen_Ioo (a := b) (b := Order.succ a) using 1
    simp [(covBy_succ_of_not_isMax ha').Ioo_eq_Ioc, hb.Ioc_eq]

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

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{u, v} (range f).card ≤ lift.{v, u} #α

Tactic:
rw [← lift_le.{max u (v + 1)}, lift_lift.{v}, lift_umax.{u, v + 1}]
  simpa [cardinalMk_coe_sort, ← coe_range, -mem_range] using mk_range_le_lift (f := f)

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

Goal state before:
pp: o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ (veblen o a).invVeblen₂ = a

Tactic:
rw [invVeblen₂_eq_iff, invVeblen₁_veblen h, ← veblen_zero_apply, veblen_veblen_of_lt]
  exact ho.bot_lt

Goal state after: