mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive

Tactic:
simp only [IsPrimitive, not_forall]

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal ≠ ⊤ → ∃ x, ∃ (_ : C x ∣ p), ¬IsUnit x
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ n, IsLocalization.mk' R' r s ^ n • f x ∈ ⊥

Tactic:
← IsLocalizedModule.mk'_one S f,

Goal state after:
case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t
⊢ IsLocalization.mk' R' r s ∈ p ↔ ∃ n, IsLocalization.mk' R' r s ^ n • IsLocalizedModule.mk' f x 1 ∈ ⊥
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case h₂
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation inv✝ ≤ 1

Tactic:
exact v.intValuation_le_one _

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

Goal state before:
pp: case zero
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
⊢ hI.dpow 0 a = 1

Tactic:
hI.dpow_zero ha

Goal state after:
case zero
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
⊢ 1 = 1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case empty
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
⊢ 1 = hI.dpow 0 a

Tactic:
hI.dpow_zero ha

Goal state after:
case empty
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
⊢ 1 = 1
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then 1 else 0) = 0

Tactic:
if_neg hn

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≠ 0
⊢ 0 = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert.h
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dpow (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

Tactic:
apply congr_arg₂ _ rfl

Goal state after:
case insert.h
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
⊢ (fun x ↦ f (hI.dpow x.1 a✝ * hI.dpow x.2 b✝)) = fun k ↦ hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
ext k

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
a✝ b✝ : A
hx : a✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n a✝) = hJ.dpow n (f a✝)
hy : b✝ ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n b✝) = hJ.dpow n (f b✝)
n : ℕ
k : ℕ × ℕ
⊢ f (hI.dpow k.1 a✝ * hI.dpow k.2 b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ (algebraMap R A) r ^ n • hI.dpow n (g m) = r ^ n • hI.dpow n (g m)

Tactic:
← map_pow,

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ (algebraMap R A) (r ^ n) • hI.dpow n (g m) = r ^ n • hI.dpow n (g m)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x✝ : Sym ι n
a✝ : x✝ ∈ x.support.sym n
i : ι
hi : i ∈ x.support
⊢ (algebraMap A S) (x i) ^ Multiset.count i ↑x✝ * hJ.dpow (Multiset.count i ↑x✝) (b i) =
    (fun i r ↦ r ^ Multiset.count i ↑x✝ • hJ.dpow (Multiset.count i ↑x✝) (b i)) i (x i)

Tactic:
← map_pow,

Goal state after:
A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x✝ : Sym ι n
a✝ : x✝ ∈ x.support.sym n
i : ι
hi : i ∈ x.support
⊢ (algebraMap A S) (x i ^ Multiset.count i ↑x✝) * hJ.dpow (Multiset.count i ↑x✝) (b i) =
    (fun i r ↦ r ^ Multiset.count i ↑x✝ • hJ.dpow (Multiset.count i ↑x✝) (b i)) i (x i)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
n : ℕ
r : R
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)

Tactic:
← map_pow,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
n : ℕ
r : R
a : M
⊢ (algebraMap R S) (r ^ n) • dp S n (f a) = r ^ n • dp S n (f a)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₁ : rs₀ ++ b :: a :: t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
this : Ideal.ofList [b, a] = Ideal.ofList [a, b]
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t

Tactic:
rw [List.append_cons, List.append_cons, List.append_assoc _ [b] [a]] at H₁

Goal state after:
case swap
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
a b : R
t rs₀ : List R
H₁ : rs₀ ++ ([b] ++ [a]) ++ t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
this : Ideal.ofList [b, a] = Ideal.ofList [a, b]
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
  (TensorProduct.cancelBaseChange R T T (T ⊗[R] S) S).trans (TensorProduct.assoc R R T T S S)
this : TensorProduct.lmul' T = (TensorProduct.map (AlgHom.id T T) (TensorProduct.lmul' R)).comp ↑e
⊢ (TensorProduct.lmul' R).Flat

Tactic:
· exact WeaklyEtale.flat_lmul' R S

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hK : K ∈ insert ⊤ {J | S ⊆ ↑J.carrier}
this : S ⊆ ↑K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ S
⊢ hI.dpow n x ∈ ↑K.carrier

Tactic:
exact K.dpow_mem n hn x (this hx)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f

Tactic:
simp only [RingHom.sub_mem_ker_iff, ← hf.2 a ha, ← hf.2 b hb]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'

Tactic:
rw [Ideal.map, span_le]

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ ⇑f '' ↑I ⊆ ↑(hK.dpEqualizer hK')
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
← map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f (a * b)) = f a ^ n * f (hI.dpow n b)

Tactic:
← map_pow,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : f b ∈ J
⊢ dpow hI f n (f (a * b)) = f (a ^ n) * f (hI.dpow n b)
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
⊢ φ ζ ^ k = 1

Tactic:
← map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
⊢ φ (ζ ^ k) = 1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIJ hIf).dpow n (f a) = f (hI.dpow n a)

Tactic:
by
  rw [dpow_def, dpow_apply' hI hIf ha]

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ φ ζ ^ j - ζ ^ (q * j) ∈ Q

Tactic:
← map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ φ (ζ ^ j) - ζ ^ (q * j) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝³ : Algebra.IsIntegral R S
this✝² : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
r : R ⧸ P
⊢ (algebraMap (R ⧸ P) (S ⧸ Q)) r ^ p ^ ↑k = (algebraMap (R ⧸ P) (S ⧸ Q)) r

Tactic:
← map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝³ : Algebra.IsIntegral R S
this✝² : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
r : R ⧸ P
⊢ (algebraMap (R ⧸ P) (S ⧸ Q)) (r ^ p ^ ↑k) = (algebraMap (R ⧸ P) (S ⧸ Q)) r
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
⊢ map (g.comp f) N = map g (map f N)

Tactic:
algebraize [f.toRingHom, g.toRingHom, (g.comp f).toRingHom]

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
⊢ map (g.comp f) N = map g (map f N)
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
c : C
m : M
⊢ fAC (c ⊗ₜ[R] m) = (↑e ∘ₗ fBC) (c ⊗ₜ[R] m)

Tactic:
simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]

Goal state after:
case tmul
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
c : C
m : M
⊢ c ⊗ₜ[A] Submodule.Quotient.mk (1 ⊗ₜ[R] m) =
    (cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[B] fAB (1 ⊗ₜ[R] m))
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ ∑ᶠ (i : ℕ), (if i = 0 then r • (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

Tactic:
finsum_eq_single _ 0 fun n hn => by simp [hn]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : VAddAntidiagonal x ⋯ = ∅
⊢ ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff x ≠ 0

Tactic:
not_not,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : VAddAntidiagonal x ⋯ = ∅
⊢ ((of R).symm (s ab.1 • (of R) (t ab.2))).coeff x = 0
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
⊢ PowerSeries.mk (f * g).coeff = PowerSeries.mk f.coeff * PowerSeries.mk g.coeff

Tactic:
by
    ext n
    simp only [PowerSeries.coeff_mul, PowerSeries.coeff_mk, coeff_mul]
    classical
    refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _
    ext m
    simp only [HasAntidiagonal.mem_antidiagonal, Finset.mem_antidiagonal, and_congr_left_iff,
      mem_filter, mem_support]
    rintro h
    rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

Goal state after: