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 ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1.le_succ_of_le
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m k✝ : ℕ
hle : n ≤ k✝
xk : R
⊢ R

Tactic:
choose x hx using h xk
      use x

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j ∈ Finset.range (k + 1)
hx : (i, j) ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Tactic:
Finset.mem_range

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1
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:
add_comm _ (C (p : ℚ) * X (n + 1)),

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))))) =
    C ↑p * X (n + 1) + (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) -
      (∑ 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.Verschiebung

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

Tactic:
simp only [verschiebungPoly, ite_true, map_zero, verschiebungFun_coeff_zero]

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
exact RingHom.ext fun x => m.equiv.injective <| (m.equiv.apply_symm_apply _).trans
      <| show Perfection.lift p R S (π.comp f) x = RingHom.comp (↑m.equiv) f x from
        RingHom.ext_iff.1 (by rw [← Equiv.eq_symm_apply]; rfl) _

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 (wittMul p x✝) ![x✝¹.coeff, y✝.coeff]

Tactic:
exact mul_coeff _ _ _

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

Goal state before:
pp: case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
hj : 0 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff 0 ^ p = 0

pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
n✝ : ℕ
hj : n✝ + 1 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff (n✝ + 1) ^ p = 0

Tactic:
· rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
n✝ : ℕ
hj : n✝ + 1 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff (n✝ + 1) ^ p = 0
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 : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r = 0

Tactic:
· rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]; exact hp

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 : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) ^ p = x.coeff m ^ (p ^ n * p)

Tactic:
pow_mul

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) ^ p = (x.coeff m ^ p ^ 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 : ℕ
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
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

Tactic:
by_cases hvp : v p = 0

Goal state after:
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
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

case neg
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
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C (↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * ⅟↑p ^ n))) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) * ↑p)

Tactic:
C_inj

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * ⅟↑p ^ n)) =
    (Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) * ↑p
Module: Mathlib.RingTheory.WittVector.Frobenius

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

Tactic:
rw [frobeniusPoly_zmod]

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

Goal state before:
pp: case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
Finset.mem_range

Goal state after:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
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 : ℕ
⊢ ↑p ^ (n + 1) ∣ x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i

Tactic:
rw [← Ideal.mem_span_singleton, mem_span_p_pow_iff_le_coeff_eq_zero,
      ← le_coeff_eq_iff_le_sub_coeff_eq_zero]
  intro i hi
  rw [WittVector.sum_coeff_eq_coeff_sum]
  · rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]
    let g := fun x : ℕ ↦ (0 : R)
    rw [Finset.sum_congr rfl (g := g)]
    · simp [g]
    · intro b hb
      simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb
      exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm
  · refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩
    ext
    dsimp only [ne_eq, Set.mem_ofPred_eq]
    rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]
    exact Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

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

Goal state before:
pp: case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case succ.zero
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hnk : Odd (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
by
  induction n generalizing k with
  | zero =>
    rw [zero_add k] at hnk
    exact coeff_hermite_of_lt hnk.pos
  | succ n ih =>
    cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two

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

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

Tactic:
(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1),

Goal state after:
case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
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)
hc :
  1 - a.coeff f.natDegree * b.coeff (f.natDegree - f.natDegree) =
    ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
Nat.sub_self

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)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsRightCancelMulZero R ∧ IsCancelAdd Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R

Tactic:
MulOpposite.isCancelAdd_iff

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ IsRightCancelMulZero R ∧ IsCancelAdd R ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n

Tactic:
Finset.mem_range

Goal state after:
case e_a.a.h
n m : ℕ
hm : m < n + 1
⊢ m ≤ n
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : 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 : ι
t : F i ⊗[R] N
⊢ (LinearMap.rTensor N (f ⋯)) (LinearMap.id t) = LinearMap.id t

Tactic:
apply DFunLike.congr_fun

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : 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 : ι
t : F i ⊗[R] N
⊢ LinearMap.rTensor N (f ⋯) = LinearMap.id
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : 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 : F k ⊗[R] N
⊢ (LinearMap.rTensor N (f h' ∘ₗ f h)) t = (LinearMap.rTensor N (f ⋯)) t

Tactic:
apply DFunLike.congr_fun

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : 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 : F k ⊗[R] N
⊢ LinearMap.rTensor N (f h' ∘ₗ f h) = LinearMap.rTensor N (f ⋯)
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 : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) (LinearMap.id t) = LinearMap.id t

Tactic:
apply DFunLike.congr_fun

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 : ι
t : M ⊗[R] F i
⊢ LinearMap.lTensor M (f ⋯) = LinearMap.id
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' ∘ₗ f h)) t = (LinearMap.lTensor M (f ⋯)) t

Tactic:
apply DFunLike.congr_fun

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) = LinearMap.lTensor M (f ⋯)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
obtain rfl | hz := eq_or_ne z 0; · simp
  ext p
  rw [mem_primeFactors, mem_normalizedFactors_iff' hz, irreducible_iff_prime,
    Int.nonneg_iff_normalize_eq_self, Finset.mem_map, Function.Embedding.coeFn_mk]
  refine ⟨fun ⟨pp, nnp, dp⟩ ↦ ?_, fun h ↦ ?_⟩
  · lift p to ℕ using nnp
    rw [← Nat.prime_iff_prime_int] at pp
    rw [Int.natCast_dvd] at dp
    exact ⟨p, by simp_all, rfl⟩
  · simp_rw [Nat.mem_primeFactors, Function.Embedding.toFun_eq_coe, Nat.castEmbedding_apply] at h
    obtain ⟨n, ⟨pn, dn, -⟩, rfl⟩ := h
    rw [Int.natCast_dvd, ← Nat.prime_iff_prime_int]
    exact ⟨pn, by simp, dn⟩

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
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'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')

Tactic:
have : ∃ q : MvPolynomial (Fin t.card) R ⊗[R] M, rTensor M (toLinearMap (φ R t).rangeRestrict) q =
      rTensor M ((Subalgebra.inclusion (le_of_eq hB)).comp
        (Subalgebra.inclusion hAB)).toLinearMap u :=
    rTensor_surjective _ (rangeRestrict_surjective _) _

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'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
this :
  ∃ q,
    (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
      (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ g.IsWeierstrassDivisorAt (IsLocalRing.maximalIdeal A)

Tactic:
IsWeierstrassDivisorAt,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ IsUnit ((coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g)