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

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a ∈ antidiagonal (optionElim k x),
    (coeff a.1) p * (coeff a.2) q =
      (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.1
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.1))
          p *
        (coeff
            (optionElim ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.fst.2
              ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩.snd.2))
          q

Tactic:
intros; simp_all [Finsupp.ext_iff]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ ↑e'.symm ∘ₗ B.ρ h = (MonoidHom.comp A.ρ ↑e.symm) h ∘ₗ ↑e'.symm

Tactic:
rw [LinearEquiv.toLinearMap_symm_comp_eq, ← LinearMap.comp_assoc]

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = (↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h) ∘ₗ ↑e'.symm
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
specialize hf (show n ≤ m by lia)

Goal state after:
case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n ≡ f m [SMOD maximalIdeal A ^ n • ⊤]
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
⊢ ↑((ofPowSMul I M b) x) a = 0

Tactic:
rw [map_val_apply]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (↑x a) = 0
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
this : IsAdicComplete (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries Unit R)
⊢ IsAdicComplete (Ideal.span {X}) R⟦X⟧

Tactic:
rwa [Set.range_unique] at this

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
⊢ (mapShortComplexH2 f 0).τ₃ = Hom.τ₃ 0

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₁ = (𝟙 (shortComplexH2 A)).τ₁

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₂ = (𝟙 (shortComplexH2 A)).τ₂

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)).τ₃ = (𝟙 (shortComplexH2 A)).τ₃

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

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

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ∏ i ∈ insert a✝ s✝, hI.dpow (n i) a = ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a

Tactic:
prod_insert hi,

Goal state after:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ hI.dpow (n a✝) a * ∏ x ∈ s✝, hI.dpow (n x) a = ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ∏ i ∈ insert a✝ s✝, dp R (n i) m = ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m

Tactic:
prod_insert hi,

Goal state after:
case insert
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ dp R (n a✝) m * ∏ x ∈ s✝, dp R (n x) m = ↑(multinomial (insert a✝ s✝) n) * dp R ((insert a✝ s✝).sum n) m
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 : ℕ
⊢ f (hI.dpow n (a✝ + b✝)) = hJ.dpow n (f a✝ + f b✝)

Tactic:
rw [hI.dpow_add hx.1 hy.1, map_sum,
      hJ.dpow_add (hf (mem_map_of_mem f hx.1)) (hf (mem_map_of_mem f hy.1))]

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 : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n, f (hI.dpow x.1 a✝ * hI.dpow x.2 b✝) =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)
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
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
⊢ hJ.dpow n (f x) = f (hI.dpow n x)

Tactic:
have hS' : S ⊆ ideal_from_ringHom hI hJ hf := fun y hy ↦ by
      simp only [mem_coe, ideal_from_ringHom, Submodule.mem_mk]
      exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩
    rw [← span_le, ← hS] at hS'
    exact ((hS' hx).2 n).symm

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
⊢ I = ⊤

Tactic:
rcases ideal_trichotomy I with rfl | rfl | rfl <;>
    first | simp at hI | simp

Goal state after:
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
| (TensorProduct.lmul' R).Flat

Tactic:
← RingHom.Flat.ulift_iff.{u₁, u₂}

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
| (RingHom.ulift.{u₁, u₂, u_2, u_2} (TensorProduct.lmul' R).toRingHom).Flat
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale R S
inst✝ : WeaklyEtale S T
⊢ WeaklyEtale R T

Tactic:
rw [← ulift_iff.{max u₁ u₂ u₃, max u₁ u₂ u₃}] at *
  refine ⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩
  · have heq : TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T) (ULift R) =
        AlgHom.comp ((TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T)
          (ULift.{max u₁ u₂ u₃} S)).restrictScalars (ULift.{max u₁ u₂ u₃} R))
          (TensorProduct.mapOfCompatibleSMul ..) := by
      ext <;> simp
    rw [heq]
    refine .comp ?_ ?_
    · exact (flat_lmul' (ULift R) (ULift S)).mapOfCompatibleSMul
        (ULift.{max u₁ u₂ u₃} T) (ULift.{max u₁ u₂ u₃} T)
    · exact WeaklyEtale.flat_lmul' (ULift S) (ULift T)

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

Goal state before:
pp: 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 := ⋯ }
x : A
hx : x ∈ S
⊢ x = hI.dpow 1 x

Tactic:
by rw [hI.dpow_one (hS 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
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ ∃ a_1, f ↑a_1 = f a

Tactic:
use ⟨a, ha⟩

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
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose h) - a ∈ RingHom.ker f

Tactic:
rw [RingHom.mem_ker, map_sub, sub_eq_zero, h.choose_spec]

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
x : R ⧸ Ideal.under R Q
⊢ (↑↑(Ideal.quotientMap Q ↑φ ⋯)).toFun ((algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x) =
    (algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x

Tactic:
by
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact DFunLike.congr_arg (Ideal.Quotient.mk Q) (φ.commutes x)

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✝ : Q.IsPrime
⊢ Ideal.comap φ Q = Q

Tactic:
refine le_antisymm (fun x hx ↦ ?_) H.le_comap
  rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
    Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : 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⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

pp: case neg
Γ : 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⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : ¬n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
· have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by
        simpa [hz, h] using hn
      simp only [coe_image, Set.mem_image]
      use (0, 0)
      simp [this.2, this.1, h, hz, smul_smul, mul_comm]

Goal state after:
case neg
Γ : 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⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : ¬n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
⊢ Nonempty (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance
  choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)
  refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩
  apply Monotone.strictMono_of_injective
  · simpa using OrderHomClass.monotone (f c)
  · simpa using hf c

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
⊢ ∃ f,
    StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
apply hahnEmbedding_isOrderedModule

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.subst F.zeroX F.zeroX = F.zeroX

Tactic:
calc
    _ = F.toPowerSeries.subst ![0, F.toPowerSeries.subst ![0, PowerSeries.X]] := by
      have : PowerSeries.HasSubst (subst ![0, PowerSeries.X (R := R)] F.toPowerSeries) := by
        refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_
        rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.zero_X
          (by simp) F.zero_constantCoeff]
      rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]
      · congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]
      · exact HasSubst.zero_X
    _ = _ := by
      have : ![0, 0] = (0 : Fin 2 → PowerSeries R) := by ext x : 1; fin_cases x <;> rfl
      simp [← F.assoc', this, subst_zero_of_constantCoeff_zero F.zero_constantCoeff,
        PowerSeries.HasSubst.X', PowerSeries.HasSubst]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Valuation

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by
    by_cases hx : x = 0; · simp [hx]
    by_cases hy : y = 0; · simp [hy]
    rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
tfae_2_to_1 :
  (∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R),
          (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ⇑φ
f : R[X]
hf : f.Monic
a₀ : R
H : φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ φ (a - a₀) = 0
h₁ : φ (Polynomial.eval a₀ f) = 0
h₂ : φ (Polynomial.eval a₀ (derivative f)) ≠ 0
⊢ IsUnit (Polynomial.eval a₀ (derivative f))

Tactic:
by
      contrapose h₂
      rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
hmn : m ≤ m + k
⊢ c m ≡ c (m + k) [SMOD I ^ m]
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R

Tactic:
Ideal.minimalPrimes,

Goal state after:
case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : maximalIdeal R ∈ {p | I.IsMinimalPrime p}
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
V : Set A
hbasis : V ∈ B
hsub : V ⊆ (fun x ↦ x * a) ⁻¹' ↑I
⊢ Submodule.colon I {a} ∈ F

Tactic:
obtain ⟨J, hJ, rfl⟩ := hB.le hbasis

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
J : Ideal A
hJ : J ∈ F
hbasis : ↑J ∈ B
hsub : ↑J ⊆ (fun x ↦ x * a) ⁻¹' ↑I
⊢ Submodule.colon I {a} ∈ F
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I J : Ideal R
inst✝ : I.Pure
⊢ I ⊓ J = I * J

Tactic:
rw [← injective_lTensor_quotient_iff_inf_eq_mul]
  apply Module.Flat.lTensor_preserves_injective_linearMap
  exact J.injective_subtype

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this✝ : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : (IsLocalRing.maximalIdeal (Localization.AtPrime p)).height ≤ 1
⊢ p.height ≤ 1

pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ (map f I).minimalPrimes

Tactic:
· rwa [← IsLocalization.height_under p.primeCompl,
      Localization.AtPrime.under_maximalIdeal] at this

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ (map f I).minimalPrimes
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
⊢ ringKrullDim R = 1 ↔ ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

Tactic:
refine ⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
h' : IsField R
⊢ False

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
⊢ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
⊢ ringKrullDim R = 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ ↑I.height.toNat
hJ₃ : I.height ≤ J.height
⊢ Submodule.spanRank J ≤ ↑I.height

Tactic:
convert! hJ₂
    exact Cardinal.ofENat_eq_nat.mpr (ENat.natCast_toNat (I.height_ne_top hI)).symm

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ ↑I.height.toNat
hJ₃ : I.height ≤ J.height
⊢ ↑I.height ≤ ↑J.height

Tactic:
exact Cardinal.ofENat_le_ofENat_of_le hJ₃

Goal state after: