mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨x, hx'⟩) = ↑0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g

Tactic:
homogeneousCochains.d_apply

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : (Hom.hom (X.d (0 + 1))) ↑⟨x, hx'⟩ = ↑0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (compForgetAugmented G).ExtraDegeneracy

Tactic:
by
  refine
    ExtraDegeneracy.ofIso (?_ : (Arrow.mk <| terminal.from G).augmentedCechNerve ≅ _)
      (extraDegeneracyAugmentedCechNerve G)
  exact
    Comma.isoMk (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)
      (Iso.refl _) (by ext : 1; exact IsTerminal.hom_ext terminalIsTerminal _ _)

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
⊢ ((X.map (cochainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i)).Exact

Tactic:
have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ ((X.map (cochainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i)).Exact
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dArrowIso₀₁ A).hom ≫
      (shortComplexH0 A).f =
    iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
apply KernelFork.mapOfIsLimit_ι

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
this : Mono X.f := hX.mono_f
i : ℕ
⊢ ((X.map (chainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i)).Exact

Tactic:
have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
this✝ : Mono X.f := hX.mono_f
i : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ ((X.map (chainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) i)).Exact
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ single g⁻¹ ((A.ρ g⁻¹) a) + single g a ∈ boundaries₁ A

Tactic:
rw [← d₂₁_single_inv_mul_ρ_add_single g 1]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g⁻¹, g * 1) ((A.ρ g⁻¹) a) + single (g, 1) a) ∈ boundaries₁ A
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
have ha₂ := span_notMem_kaplanskySet ha H

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(shortComplexH0 A).X₂
hx : (Coinvariants.mk A.ρ) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Tactic:
rw [Coinvariants.mk_eq_zero, ← range_d₁₀_eq_coinvariantsKer] at hx

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(shortComplexH0 A).X₂
hx : x ∈ (ModuleCat.Hom.hom (d₁₀ A)).range
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ P.FG ↔ (Ideal.map constantCoeff P).FG

Tactic:
constructor
  · exact (FG.map · _)
  · intro ⟨S, hS⟩
    by_cases hX : X ∈ P
    · have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS
      have : (insert X <| (C (R := R)) '' S).Finite :=
        Finite.insert X <| Finite.image _ S.finite_toSet
      lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT
      exact ⟨T, hT ▸ H.symm⟩
    · obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet
      lift T to Finset R⟦X⟧ using hT₂
      exact ⟨T, hT.symm⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)
_h' : ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen[inst✝¹] {0}

Tactic:
simpa using h 1

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
f : R →+* S
hf : Ideal.map f i ≤ i
⊢ ContinuousAt (⇑f) 0

Tactic:
by
  rw [ContinuousAt, map_zero, i.hasBasis_nhds_zero_adic.tendsto_iff i.hasBasis_nhds_zero_adic]
  refine fun n _ ↦ ⟨n, trivial, Ideal.map_le_iff_le_comap.mp ?_⟩
  simpa [Ideal.map_pow] using Ideal.pow_right_mono hf n

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R)

Tactic:
IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg',

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R)) =
    Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R)
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: case cons
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ↑s ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑s
hs : IsGroupLikeElem R a ∧ ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id ↑(Finset.cons a s has)

Tactic:
obtain ⟨ha, hs⟩ := hs

Goal state after:
case cons
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ih : ↑s ⊆ {a | IsGroupLikeElem R a} → LinearIndepOn R id ↑s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
⊢ LinearIndepOn R id ↑(Finset.cons a s has)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ mapDomainOfBialgHomFun f (g₁ * g₂) = mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂

Tactic:
by
    refine single_left_injective (R := R) one_ne_zero ?_
    simp only [single_mapDomainOfBialgHomFun_one]
    rw [← mul_one (1 : R), ← single_mul_single, ← single_mul_single, map_mul]
    simp

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
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {r | IsSMulRegular M r}ᶜ

Tactic:
by
    simp_rw [Set.compl_ofPred, isSMulRegular_iff_right_eq_zero_of_smul,
      not_forall, exists_prop, and_comm]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x✝ : A
ha : x✝ ∈ ⊥
⊢ (if x✝ = 0 ∧ 0 = 0 then 1 else 0) = 1

Tactic:
by
    rw [mem_bot.mp ha]
    simp only [and_self, ite_true]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ (k + n i).choose k • (dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)) ∈
    Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)

Goal state after:
case dp.mem.mem
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ (fun n ↦ n.prod fun i k ↦ dp R k (v i)) (Finsupp.single i k + n) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ (↑m !)⁻¹ʳ * 0 =
    ∑ k ∈ Finset.antidiagonal m, (if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ 0 =
    ∑ k ∈ Finset.antidiagonal m, (if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * 0) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * 0 = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * 0 = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ 0 = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ 0 = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ 0 = ↑((m + k).choose m) * 0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * (↑k !)⁻¹ʳ ^ m * 0 = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * 0)

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ 0 = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * 0)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ 0 = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * 0)

Tactic:
mul_zero,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ 0 = ↑(m.uniformBell k) * 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
⊢ hI.IsSubDPIdeal (J ⊔ K)

Tactic:
rw [← J.span_eq, ← K.span_eq, ← span_union,
    span_isSubDPIdeal_iff (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)]
  intro n hn a ha
  rcases ha with ha | ha
  · exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))
  · exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0

Tactic:
exact hn.le (Ideal.pow_mem_pow haI _)

Goal state after:
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 k R
f : R →ₐ[k] k
x✝ : R
this : (RingHom.ker f).IsPrime
⊢ (Ideal.Quotient.mk (RingHom.ker f)) x✝ = (algebraMap R (R ⧸ RingHom.ker f)) ((algebraMap k R) (f x✝))

Tactic:
simp [-Ideal.Quotient.mk_algebraMap, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: case refine_1
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
⊢ (AlgHom.id T T).Flat

Tactic:
exact .of_bijective Function.bijective_id

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ ∀ (s : Fin (Nat.succ 0).succ), IsNilpotent (constantCoeff (![f, g] s))

Tactic:
by simp [hf, hg]

Goal state after:
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⟦Γ⟧
f : PowerSeries R
r : R
n : ℕ
⊢ (powerSeriesFamily x (r • f)) n = ((HahnSeries.single 0) r • powerSeriesFamily x f) n

Tactic:
simp [mul_smul]

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
he : ∃ c, c.1 + c.2 = n ∧ (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
obtain ⟨c, hcn, hc⟩ := he

Goal state after:
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
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 =
    ∑ x ∈ HasAntidiagonal.antidiagonal n, f.coeff x.1 * g.coeff x.2

Tactic:
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:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - (single oinv) r * (y + (single x.order) x.leadingCoeff) = -((single oinv) r * y)

Tactic:
mul_add,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - ((single oinv) r * y + (single oinv) r * (single x.order) x.leadingCoeff) = -((single oinv) r * y)
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ maximalIdeal R ≤ ⊥.jacobson

Tactic:
rw [Ideal.jacobson, le_sInf_iff]
    rintro I ⟨-, hI⟩
    exact (eq_maximalIdeal hI).ge

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (c (n + 1)) f ∈ I ^ (n + 1 + 1)

Tactic:
← taylor_eval_sub (c n),

Goal state after:
case succ
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (c (n + 1) - c n) ((taylor (c n)) f) ∈ I ^ (n + 1 + 1)