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

Goal state before:
pp: case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨x, rfl⟩ := ha

Goal state after:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
hb : ε ∣ b
x : K[ε]
⊢ ∃ c, ε * x * c = b ∨ b * c = ε * x
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ((AlgHom.ulift.{?u.31, u₁, u₂, u_1, u_2, u_2} (TensorProduct.lmul' R)).comp
        ↑(TensorProduct.uliftEquiv R (ULift.{u₁, u_1} R) S S).symm).Flat ↔
    (RingHom.ulift.{u₁, u₂, u_2, u_2} (TensorProduct.lmul' R).toRingHom).Flat

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (↑((AlgHom.ulift.{?u.31, u₁, u₂, u_1, u_2, u_2} (TensorProduct.lmul' R)).comp
          ↑(TensorProduct.uliftEquiv R (ULift.{u₁, u_1} R) S S).symm)).Flat ↔
    (RingHom.ulift.{u₁, u₂, u_2, u_2} (TensorProduct.lmul' R).toRingHom).Flat
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 : ℕ
⊢ (1 - ζ ^ ((q + k - i) * j)) * ζ ^ (i * j) ∈ Q

Tactic:
sub_mul,

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 : ℕ
⊢ 1 * ζ ^ (i * j) - ζ ^ ((q + k - i) * j) * ζ ^ (i * 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
φ : 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) - ζ ^ (j * q) ∈ Q

Tactic:
pow_mul

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) - (ζ ^ j) ^ q ∈ Q
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑(invOneSubPow S (d - 1 + 1)) = mk fun n ↦ ↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1))

Tactic:
invOneSubPow,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑{ val := mk fun n ↦ ↑((d - 1 + n).choose (d - 1)), inv := (1 - X) ^ (d - 1 + 1), val_inv := ⋯, inv_val := ⋯ } =
    mk fun n ↦ ↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1))
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
⊢ powerSeriesFamily x f = powerSeriesFamily 0 f

Tactic:
by
  ext n g
  obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

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

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (sin A)) = (coeff n✝) (sin A')

Tactic:
simp [sin, apply_ite f]

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
· replace hn := congr(Ideal.comap (Ideal.Quotient.mk I) $(hn _ n.le_succ))
    simp only [qs, OrderHom.coe_mk, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
      Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at hn
    intro x hx
    obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))
    refine Submodule.add_mem_sup hy ?_
    obtain ⟨z, rfl⟩ := (Submodule.IsPrincipal.mem_iff_eq_smul_generator I).mp hz
    rw [smul_eq_mul, smul_eq_mul, mul_comm]
    refine Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)
    dsimp [IsLocalization.orderEmbedding] at hx
    rwa [Ideal.mem_comap, f.map_add, f.map_mul, Ideal.add_mem_iff_right _
      (Ideal.pow_le_pow_right n.le_succ hy), mul_comm, Ideal.unit_mul_mem_iff_mem] at hx
    refine IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩
    change Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
    rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]
    exact fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ Function.Surjective ⇑(Hom.hom P.toLimit)

Tactic:
have : IsClosed (Set.range P.toLimit) :=
    P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range

Goal state after:
P : ProfiniteGrp.{u}
this : IsClosed (Set.range ⇑(Hom.hom P.toLimit))
⊢ Function.Surjective ⇑(Hom.hom P.toLimit)
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
⊢ Disjoint ↑(Submonoid.map C p.primeCompl) ↑P

Tactic:
refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
a : R[X]
x✝ : a ∈ ↑(Submonoid.map C p.primeCompl)
ha : a ∈ ↑P
b : R
hb : b ∈ ↑p.primeCompl ∧ C b = a
⊢ b ∈ ↑p
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p I : Ideal R
inst✝ : p.IsPrime
h : I ≤ p
⊢ ↑(Ideal.map (Ideal.Quotient.mk I) p).height + ↑(Submodule.spanFinrank I) ≤
    ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
gcongr
    have : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime :=
      Ideal.isPrime_map_quotientMk_of_isPrime h
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
hx : x ∈ maximalIdeal R
⊢ supportDim R R ≤ ringKrullDim (R ⧸ x • ⊤) + 1

Tactic:
← Module.supportDim_quotient_eq_ringKrullDim

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
hx : x ∈ maximalIdeal R
⊢ supportDim R R ≤ supportDim R (R ⧸ x • ⊤) + 1
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h : Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd) = ⊤
⊢ IsLocalIso R T

Tactic:
have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
    exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (frac { asIdeal := P, isMaximal := hP } ↑x).2 • ↑x ∈
    Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)))

Tactic:
hfrac

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (f { asIdeal := P, isMaximal := hP }.asIdeal) (frac { asIdeal := P, isMaximal := hP } ↑x).1 ∈
    Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : D + ↑s ≤ 0
⊢ D + ↑s ≤ -0

Tactic:
neg_zero

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : D + ↑s ≤ 0
⊢ D + ↑s ≤ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < -0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
neg_zero

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, w x • (X x * (pderiv x) p + X x * (pderiv x) q) = n • (p + q)

Tactic:
smul_add,

Goal state after:
case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, (w x • (X x * (pderiv x) p) + w x • (X x * (pderiv x) q)) = n • p + n • q
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ p = b * a

Tactic:
rw [hab, mul_comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ (coeff m) φ * (coeff (p • m)) (m.prod fun s e ↦ (X s ^ p) ^ e) = (coeff m) φ

Tactic:
rw [this, coeff_monomial, if_pos rfl, mul_one]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
⊢ (↑(DistribSMul.toAddMonoidHom M (single i i 1))).toFun (r • x) =
    (RingHom.id R) r • (↑(DistribSMul.toAddMonoidHom M (single i i 1))).toFun x

Tactic:
dsimp
        have : Commute (diagonal fun x : ι ↦ r) (single i i 1) := by
          ext; simp [Matrix.single]
        rw [← smul_assoc r, smul_eq_diagonal_mul, this.eq, mul_smul, ← smul_one_eq_diagonal]
        nth_rw 1 [← one_smul (Matrix ι ι R) x]
        rw [smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
hval : Valued.v f ≤ 1
F : K⟦X⟧
hF : (ofPowerSeries ℤ K) F = f
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x

Tactic:
rw [hF, hf, RingEquiv.symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
⊢ (T1 f (-1)).comp (T1 f 1) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
simpa using t1_comp_t1_neg f (-1)

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: case succ
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ (p * p ^ m) ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]

Tactic:
pow_mul

Goal state after:
case succ
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ (Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ p) ^ p ^ m ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ Disjoint {n} (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars

Tactic:
disjoint_singleton_left

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∉ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - ∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0

Tactic:
sub_mul,

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ 1 * C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0

Tactic:
Finset.mem_range

Goal state after:
case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
Finset.mem_range

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ (p * p ^ (n - k))

Tactic:
pow_mul

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
Finset.mem_range

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k

Tactic:
revert k

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (k : ℕ), (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k
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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + C (↑p ^ n) * X n ^ p + C (↑p ^ (n + 1)) * 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_mul,

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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + C (↑p ^ n) * X n ^ p + C (↑p ^ (n + 1)) * X (n + 1)) *
        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)