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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (killComplFun e ((monomial x) r)) = (coeff n✝) 0

Tactic:
simp [coeff_killComplFun, coeff_monomial]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n✝ : σ →₀ ℕ
⊢ embDomain e n✝ = x → r = 0
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f✝ : R⟦X⟧
hf✝ : constantCoeff f✝ ∈ span S
r₁ r₂ : R
hr₁ : r₂ ∈ Submodule.span R S
f : R⟦X⟧
hfmem : f ∈ span T
hf : constantCoeff f = r₂
⊢ constantCoeff (r₁ • f) = r₁ • r₂

Tactic:
simp [hf]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst✝² : P.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
⊢ UniqueFactorizationMonoid R⟦X⟧

Tactic:
by
  refine UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.mpr (fun P h₁ h₂ ↦ ?_)
  by_cases hXP : X ∈ P
  · exact ⟨X, hXP, X_prime⟩
  · obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
    obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
    simp only [ncard_singleton, ncard_eq_one] at h
    obtain ⟨_, rfl⟩ := h
    exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsPrecomplete I R ↔ IsPrecomplete (Ideal.map e I) S

Tactic:
IsAdic.isPrecomplete_iff (by rfl),

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ CompleteSpace R ↔ IsPrecomplete (Ideal.map e I) S
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
⊢ IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R

Tactic:
let : WithIdeal R := ⟨I⟩
  let : WithIdeal S := ⟨I.map e⟩
  rw [iff_comm, IsAdic.isHausdorff_iff rfl, IsAdic.isHausdorff_iff rfl]
  exact ⟨fun _ ↦ (WithIdeal.uniformEquiv e rfl).toHomeomorph.t2Space, fun _ ↦
    (WithIdeal.uniformEquiv e rfl).toHomeomorph.symm.t2Space⟩

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
⊢ 0 = (coeff y) ((monomial x.some) r)

Tactic:
replace h1 : ¬ y = x.some := fun h ↦ by
      absurd h1; ext u
      cases u <;> simp_all

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h3 : n = x none
h1 : ¬y = x.some
⊢ 0 = (coeff y) ((monomial x.some) r)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < 0
⊢ ↑((J ^ 0) ^ m) ⊆ ↑(J ^ m)

pp: case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑((J ^ (n✝ + 1)) ^ m) ⊆ ↑(J ^ m)

Tactic:
· exfalso
      exact Nat.not_succ_le_zero 0 hn

Goal state after:
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑((J ^ (n✝ + 1)) ^ m) ⊆ ↑(J ^ m)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I m : Ideal R
inst✝ : m.IsMaximal
le : I ≤ m
fg : I.FG
⊢ (Ideal.map (algebraMap R (AdicCompletion I R)) m).IsMaximal

Tactic:
have mapeq : m.map (algebraMap R (AdicCompletion I R)) = (m.map (Ideal.Quotient.mk I)).comap
    (AdicCompletion.evalOneₐ I).toRingHom := by
    rw [← AdicCompletion.evalOneₐ_comp_algebraMap_eq_mk, ← Ideal.map_map,
      Ideal.comap_map_of_surjective' (evalOneₐ I).toRingHom (evalOneₐ_surjective I),
      eq_comm, sup_eq_left, AdicCompletion.ker_evalOneₐ_eq_map I fg]
    exact Ideal.map_mono le
  have : (Ideal.map (Ideal.Quotient.mk I) m).IsMaximal :=
    Ideal.IsMaximal.map_of_surjective_of_ker_le Ideal.Quotient.mk_surjective (by simpa using le)
  rw [mapeq]
  exact Ideal.comap_isMaximal_of_surjective _ (evalOneₐ_surjective I)

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
⊢ (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
by
  ext
  simp [chainsMap_f, Unique.eq_default (α := Fin 0 → G), Unique.eq_default (α := Fin 0 → H),
    chainsIso₀]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p q : R[X]
hpq : p ∣ q
⊢ q.contentIdeal ≤ p.contentIdeal

Tactic:
obtain ⟨p', rfl⟩ := hpq

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p p' : R[X]
⊢ (p * p').contentIdeal ≤ p.contentIdeal
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : a✝ ∈ p.coeffs
⊢ a✝ ∈ ↑(span {p.content})

Tactic:
mem_coeffs_iff

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
h1 : ∃ n ∈ p.support, a✝ = p.coeff n
⊢ a✝ ∈ ↑(span {p.content})
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: 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 : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

Tactic:
classical
  rw [show v.valuation K x = _ * _ by rw [valuation_def]; rfl]
  rw [Units.val_inv_eq_inv_val]
  change _ = ite _ _ _ * (ite _ _ _)⁻¹
  simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0 → ⟨a, b⟩ = 0) ↔ ∀ x ∈ N, r • x = 0 → x = 0

Tactic:
simp only [SetLike.mk_smul_mk, Submodule.mk_eq_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)

Tactic:
by
  intro (h : Function.Injective (DistribSMul.toLinearMap R M r))
  rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h,
    ← LinearMap.lsmul_eq_distribSMultoLinearMap,
    map_comap_eq, LinearMap.range_eq_map]; rfl

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

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ (∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) = 0

Tactic:
apply sum_eq_zero

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ ∀ x ∈ antidiagonal n✝, (if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) = 0
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
x✝¹ x✝ : M
⊢ dp R 1 (x✝¹ + x✝) = dp R 1 x✝¹ + dp R 1 x✝

Tactic:
by simp [dp_add, Nat.antidiagonal_succ, dp_zero, add_comm]

Goal state after:
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
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n✝ (g (f a)) = g (f (hI.dpow n✝ a))

Tactic:
← hf.2 a ha,

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
C : Type u_3
inst✝ : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n✝ (g (f a)) = g (hJ.dpow n✝ (f a))
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 : ℕ
k : ℕ × ℕ
⊢ f (hI.dpow k.1 a✝ * hI.dpow k.2 b✝) = hJ.dpow k.1 (f a✝) * hJ.dpow k.2 (f b✝)

Tactic:
rw [map_mul, hx.2, hy.2]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1

Tactic:
· simp [hn]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
hiff : ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1) ↔ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
⊢ ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ (↑p)⁻¹

Tactic:
exact dpow'_norm_le_of_ne_zero p hm hx

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔
    ∃ c, TrivSqZeroExt.fst x = TrivSqZeroExt.fst (ε * c) ∧ TrivSqZeroExt.snd x = TrivSqZeroExt.snd (ε * c)

Tactic:
TrivSqZeroExt.fst_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔
    ∃ c,
      TrivSqZeroExt.fst x = TrivSqZeroExt.fst ε * TrivSqZeroExt.fst c ∧ TrivSqZeroExt.snd x = TrivSqZeroExt.snd (ε * c)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
inst✝ : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ Module.FinitePresentation R S

Tactic:
apply Module.FinitePresentation.of_equiv e.symm.toLinearEquiv

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
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
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = f (hI.dpow k.1 a) * f (hI.dpow k.2 b)

Tactic:
← _root_.map_mul

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 : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = f (hI.dpow k.1 a * hI.dpow k.2 b)
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (binomialFamily x r) n = 0 ^ n

Tactic:
binomialFamily,

Goal state after:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (powerSeriesFamily (x - 1) (PowerSeries.binomialSeries A r)) n = 0 ^ n
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)

Tactic:
ext1 i

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
i : Fin (Nat.succ 0).succ
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] i = (MvPowerSeries.map f) (![g₁, g₂] i)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)

Tactic:
refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.constantCoeff (subst ![PowerSeries.X, 0] F.toPowerSeries) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] s)) F.toPowerSeries =
    subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
· congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)

Tactic:
refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.constantCoeff (subst ![0, PowerSeries.X] F.toPowerSeries) = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 ↦ x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 ↦ x1 + x2) i j → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff ((fun x1 x2 ↦ x1 + x2) i j) ≠ 0}
⊢ (j, i) ∈ ↑(antidiagonal ⋯ hpwo ((fun x1 x2 ↦ x1 + x2) i j))

Tactic:
simp only [mem_coe, mem_antidiagonal, mem_support, ne_eq, Set.mem_iUnion]

Goal state after:
case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 ↦ x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 ↦ x1 + x2) i j → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff ((fun x1 x2 ↦ x1 + x2) i j) ≠ 0}
⊢ ¬x.coeff j = 0 ∧ (∃ i_1, ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ [HenselianLocalRing R,
      ∀ (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₀,
      ∀ {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₀].TFAE

Tactic:
by
  tfae_have 3 → 2
  | H => H (residue R) Ideal.Quotient.mk_surjective
  tfae_have 2 → 1
  | H => by
    constructor
    intro f hf a₀ h₁ h₂
    specialize H f hf (residue R a₀)
    have aux := flip mem_nonunits_iff.mp h₂
    simp only [aeval_def, ResidueField.algebraMap_eq, eval₂_at_apply, ←
      Ideal.Quotient.eq_zero_iff_mem, ← IsLocalRing.mem_maximalIdeal] at H h₁ aux
    obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux
    refine ⟨a, ha₁, ?_⟩
    rw [← Ideal.Quotient.eq_zero_iff_mem]
    rwa [← sub_eq_zero, ← map_sub] at ha₂
  tfae_have 1 → 3
  | hR, K, _K, φ, hφ, f, hf, a₀, h₁, h₂ => by
    obtain ⟨a₀, rfl⟩ := hφ a₀
    have H := HenselianLocalRing.is_henselian f hf a₀
    simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
    obtain ⟨a, ha₁, ha₂⟩ := H h₁ (by
      contrapose h₂
      rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂)
    refine ⟨a, ha₁, ?_⟩
    rwa [φ.map_sub, sub_eq_zero] at ha₂
  tfae_finish

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

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [hx] at iu

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ IsUnit x
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✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
q : ℚ
x : R⟦Γ⟧
⊢ q • x = ↑q * x

Tactic:
by ext; simp [← single_zero_ratCast, Rat.smul_def]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ HopfAlgebra R B

Tactic:
refine .ofConvInverse (antipode R) (ofConv_injective ?_) (ofConv_injective ?_)

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1

case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv = ofConv 1
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ IsIdempotentElem I

Tactic:
by
  simp [IsIdempotentElem, ← Ideal.inf_eq_mul_of_pure]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
⊢ Module.Flat R (R ⧸ I)

Tactic:
Module.Flat.iff_lTensor_injective

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype I_1))
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ supportDim R M = ringKrullDim (R ⧸ annihilator R M)

Tactic:
by
  simp only [supportDim]
  rw [support_eq_zeroLocus, ringKrullDim_quotient]

Goal state after:
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
ι : Type u_3
f : ι → S
h : ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
this : { asIdeal := q, isPrime := hq } ∈ ⨆ i, PrimeSpectrum.basicOpen (f i)
⊢ ∃ i, f i ∉ q

Tactic:
simpa using this

Goal state after:
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)
⊢ IsLocalIso R T

Tactic:
let (g : S) : Algebra (Localization.Away g) (T' g) := localizationAlgebra (.powers g) T

Goal state after:
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
⊢ IsLocalIso R T