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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n)) =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
wittStructureRat_rec_aux

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)) =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝ }.coeff n = y.coeff n
⊢ { coeff := coeff✝ } = y

Tactic:
cases y

Goal state after:
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝¹ }.coeff n = { coeff := coeff✝ }.coeff n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + n - m = j + i + (n - i - m)

Tactic:
add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + i + (n - i - m)
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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ h (f x_1) (g y)

Tactic:
refine ⟨⟨fun n ↦ bind₁ (uncurry <|
    ![fun k ↦ rename (Prod.mk (0 : Fin 2)) (φ k),
      fun k ↦ rename (Prod.mk (1 : Fin 2)) (ψ k)]) (χ n), ?_⟩⟩

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
φ : ℕ → 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)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R),
    (h (f x) (g y)).coeff = fun n ↦
      peval
        ((fun n ↦ (bind₁ (uncurry ![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)])) (χ n)) n)
        ![x.coeff, y.coeff]
Module: Mathlib.RingTheory.WittVector.Identities

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

Tactic:
by
  rw [coeff_p, if_neg]
  exact zero_ne_one

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

Goal state before:
pp: case refine_3
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 : ℕ
⊢ (ghostComponent n) (select P x + select (fun i ↦ ¬P i) x) = (ghostComponent n) x

Tactic:
simp only [map_add]

Goal state after:
case refine_3
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 : ℕ
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i ↦ ¬P i) x) = (ghostComponent n) x
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
f : ℕ → R
⊢ (truncate n) { coeff := f } = TruncatedWittVector.mk p fun k ↦ f ↑k

Tactic:
ext i
  simp only [coeff_truncate, TruncatedWittVector.coeff_mk]

Goal state after:
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
⊢ ∀ (f : ℕ → 𝕎 k),
    (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD Ideal.span {↑p} ^ m • ⊤]) →
      ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD Ideal.span {↑p} ^ n • ⊤]

Tactic:
by
    intro x h
    -- construct the limit Witt vector w diagonally
    use .mk p (fun n ↦ (x (n + 1)).coeff n)
    intro n
    simp only [Ideal.span_singleton_pow, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
      mem_span_p_pow_iff_le_coeff_eq_zero, ← le_coeff_eq_iff_le_sub_coeff_eq_zero] at h ⊢
    intro i hi
    exact (h hi i (Nat.lt_succ_self i)).symm

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
⊢ {y | x = y + y⁻¹ ∨ y = 0}.Finite

Tactic:
have hφ : φ ≠ 0 := by
        intro H
        have : φ.eval 0 = 0 := by rw [H, eval_zero]
        simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
          mul_zero, sq, zero_add, one_ne_zero]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
⊢ {y | x = y + y⁻¹ ∨ y = 0}.Finite
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff = (↑d !)⁻¹

Tactic:
simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

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

Goal state before:
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 DifferentiableAt.exp; simp

Goal state after:
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
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
⊢ IsUnit a ∨ IsUnit b

Tactic:
refine .inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn

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
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ ∧ p.coeff x = 0
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

Tactic:
rw [hx.2, zero_mul]

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

Goal state before:
pp: case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

pp: case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((n + d - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))

Tactic:
· simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
        rw [hx.2, zero_mul]

Goal state after:
case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((n + d - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
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
⊢ (q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly d = 0

Tactic:
← zero_add d,

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
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
⊢ (q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly (0 + d) = 0
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), (coeff i) g ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (I := ⊤) (f := f) (by simp) hg

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ (LinearMap.lTensor M (f h') ∘ₗ LinearMap.lTensor M (f h)) t = (LinearMap.lTensor M (f ⋯)) t

Tactic:
← lTensor_comp

Goal state after:
R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ (LinearMap.lTensor M (f h' ∘ₗ f h)) t = (LinearMap.lTensor M (f ⋯)) 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
r a b : R
f✝ g✝ f g h : M →ₚₗ[R] N
⊢ f + g + h = f + (g + h)

Tactic:
by ext; simp only [add_def, add_assoc]

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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
⊢ (φ R s).range.FG

Tactic:
rw [← Algebra.map_top]

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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
⊢ (Subalgebra.map (φ R s) ⊤).FG
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
⊢ (φ R s').range.FG

Tactic:
rw [← Algebra.map_top]

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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
⊢ (Subalgebra.map (φ R s') ⊤).FG
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:
induction rs generalizing M N with

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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (rTensor M (rename j).toLinearMap) p
⊢ π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t

Tactic:
simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ f.degree = ↑n

Tactic:
rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]

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
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ False

Tactic:
have : IsSemisimpleModule R c := by obtain ⟨S, _, rfl⟩ := hc; infer_instance

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this : IsSemisimpleModule R ↥c
⊢ False
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
have eq : comap C pS = maximalIdeal (Localization.AtPrime q) := by
    rw [← IsLocalization.map_under q.primeCompl _ (comap C pS),
      ← IsLocalization.map_under q.primeCompl _ (maximalIdeal (Localization.AtPrime q))]
    simp only [comap_comap, S, pS]
    rw [← Polynomial.algebraMap_eq (R := Localization.AtPrime q),
      ← IsScalarTower.algebraMap_eq R (Localization.AtPrime q) (Localization.AtPrime q)[X],
      IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime q)[X], ← comap_comap,
      ← Ideal.under_def R[X], IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj]
    simp [q, IsLocalization.AtPrime.under_maximalIdeal (Localization.AtPrime q) q]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
eq : comap C pS = maximalIdeal (Localization.AtPrime q)
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ s.sum f ∈ I

Tactic:
rw [mem_iff, ← Finset.sum_const_zero]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.23, 0)

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.28

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.21
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: case nil
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
hl : ∃ x ∈ [], f x ∈ I
⊢ (List.map f []).prod ∈ I

Tactic:
simp only [List.not_mem_nil, false_and, exists_false] at hl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 0 < ↑p

Tactic:
exact mod_cast hp.out.pos

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
⊢ ∀ ⦃s : Set (Set (List A))⦄,
    s ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T} → sInf s ∈ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}

Tactic:
by rintro S hS x a h T hT; exact hS hT <| h T hT

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
by
  rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα]
  simp

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ lfpApprox f x ↑⟨0, ⋯⟩

Tactic:
simp [lfpApprox_zero]

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

Goal state before:
pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
simp [IH i hi hi', hf]

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ (a : (_ : Ordinal.{u_1}) × Ordinal.{u_1}), (∃ a_1 ∈ CNF b o, a_1.toSigma = a) → decide (a.snd ≠ 0) = true

Tactic:
rintro _ ⟨a, ⟨ha, rfl⟩⟩

Goal state after:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
⊢ decide (a.toSigma.snd ≠ 0) = true