mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
exact h.mgf_le t

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
X Y : Rep k G
hf : Function.Surjective ⇑f
f' : res f X ⟶ res f Y
g : G
⊢ (Hom.hom f').toLinearMap ∘ₗ X.ρ g = Y.ρ g ∘ₗ (Hom.hom f').toLinearMap

Tactic:
by obtain ⟨h, rfl⟩ := hf g; simpa using f'.hom.2 h

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
obtain φ : σ.Equiv ρ := Classical.choice inferInstance
    rw [char_iso φ, card_inv_mul_sum_char_mul_char_eq_finrank]
    simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ Hom.hom f = Hom.hom g

Tactic:
ext1; dsimp; ext h; simpa using hfg h

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
h : (QuotientGroup.rightRel S) g₁ g
⊢ g₁ * g⁻¹ ∈ S

Tactic:
rcases h with ⟨s, rfl⟩; exact mul_inv_cancel_right s.1 g ▸ s.2

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
⊢ QuasiIsoAt (resolution.π k g) m

Tactic:
by
    induction m with
    | zero =>
      simp only [resolution.π]
      rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]
      constructor
      · apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful
        simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using!
          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg
      · rw [Rep.epi_iff_surjective]
        intro x
        use .single 1 x
        simp [ChainComplex.toSingle₀Equiv]
    | succ m _ =>
      rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
      apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful
      rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
      by_cases hm : Odd (m + 1)
      · simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
          if_neg (Nat.not_even_iff_odd.2 hm)]
          using! leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg
      · simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
          if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)]
        using! leftRegular.range_applyAsHom_sub_eq_ker_norm k g hg

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ ∀ (i j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      (freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm.hom ≫ ((barComplex k G).linearYonedaObj k A).d i j =
        (inhomogeneousCochains A).d i j ≫ (freeLiftLEquiv k G (Fin j → G) A).toModuleIso.symm.hom

Tactic:
rintro i j (h : i + 1 = j)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
i j : ℕ
h : i + 1 = j
⊢ (freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm.hom ≫ ((barComplex k G).linearYonedaObj k A).d i j =
    (inhomogeneousCochains A).d i j ≫ (freeLiftLEquiv k G (Fin j → G) A).toModuleIso.symm.hom
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ (resFunctor φ).obj Y✝
⊢ (indResHomEquiv φ X'✝ Y✝).toEquiv.symm (x✝¹ ≫ x✝) =
    (indFunctor k φ).map x✝¹ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝

Tactic:
by
      change (indResHomEquiv φ _ _).symm (_ ≫ _) = _
      ext; simp [indMap, indResHomEquiv]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isCocycle₂ hf g] at this

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ map (MonoidHom.id G) (φ ≫ ψ) n = map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝ : G
⊢ rightFDRep.ρ x✝ ≫ InducedCategory.homMk (↟(leftRegular s)) =
    InducedCategory.homMk (↟(leftRegular s)) ≫ rightFDRep.ρ x✝

Tactic:
by
    ext f
    funext _
    apply congrArg f
    exact mul_assoc ..

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ renameFun f 0 = 0

Tactic:
by ext; simp [coeff_renameFun]

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

Goal state before:
pp: case refine_3
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₂
⊢ ∃ x ∈ span T, constantCoeff x = r₁ • r₂

Tactic:
exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (if Finsupp.cons k x = single j.succ 1 then 1 else 0) = (coeff x) (if k = 0 then X j else 0)

Tactic:
cons_eq_single_succ_iff

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (if x = single j 1 ∧ k = 0 then 1 else 0) = (coeff x) (if k = 0 then X j else 0)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
n : ℕ
⊢ map (g.comp f) (φ ≫ (resFunctor f).map ψ) n = map f φ n ≫ map g ψ n

Tactic:
by
  simp [map, ← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]

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 : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B

Tactic:
by
      have := congr($((mapShortComplexH1 f φ).comm₂₃) x); simp_all [cycles₁, shortComplexH1]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
have h : (Algebra.TensorProduct.comm R (SymmetricAlgebra R M)
          (SymmetricAlgebra R M)).toAlgHom.comp (Bialgebra.comulAlgHom R _) =
        Bialgebra.comulAlgHom R (SymmetricAlgebra R M) := by
      ext x
      simp
      abel
    exact congr(($h).toLinearMap)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p ≠ 0 → ∃ x ∈ ↑p.coeffs, x ≠ 0

Tactic:
exact fun h ↦ ⟨p.leadingCoeff, coeff_mem_coeffs (leadingCoeff_ne_zero.mpr h),
    leadingCoeff_ne_zero.mpr h⟩

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
N : Type u_9
O : Type u_10
inst✝³ : CommSemiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
x✝ : R[M]
a✝ : O
⊢ ((mapDomainBialgHom R (f.comp g)) x✝).coeff a✝ = (((mapDomainBialgHom R f).comp (mapDomainBialgHom R g)) x✝).coeff a✝

Tactic:
simp [Finsupp.mapDomain_comp]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Tactic:
by
  by_cases hp0 : p = 0
  · simp [hp0]
  have hsupp_nonempty : p.support.Nonempty := by grind [support_nonempty]
  simp only [gaussNorm, hsupp_nonempty, ↓reduceDIte, one_pow, mul_one, contentIdeal, Ideal.span_le,
    Set.subset_def, SetLike.mem_coe, ← v.intAdicAbv_lt_one_iff hb]
  constructor
  · contrapose!
    simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]
    intro _ h1 h2
    exact Finset.le_sup'_of_le (fun n ↦ (v.intAdicAbv hb) (p.coeff n)) (by simp [h1]) h2
  · intro h
    rw [Finset.sup'_lt_iff]
    intro n hn
    rw [mem_support_iff] at hn
    exact h _ <| p.coeff_mem_coeffs hn

Goal state after:
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
n : ℕ
x : Rˣ
⊢ (v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1

Tactic:
erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
    QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),
    valuation_of_unit_eq, QuotientGroup.mk_one, map_one]

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
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ ((LinearMap.lsmul R M) r).range ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
LinearMap.range_eq_map

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁹ : CommRing R'
inst✝⁸ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
f : M →ₗ[R] M'
inst✝³ : IsLocalizedModule S f
inst✝² : Module R' M'
inst✝¹ : IsScalarTower R R' M'
inst✝ : IsNoetherianRing R
⊢ Ideal.comap (algebraMap R R') ⁻¹' associatedPrimes R M = associatedPrimes R' M'

Tactic:
by
  ext p
  exact ⟨mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule S f p,
    fun h ↦ comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg S f p h
    ((isNoetherianRing_iff_ideal_fg R).mp ‹_› _)⟩

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

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

Tactic:
rw [if_neg hn, if_neg]

Goal state after:
case neg.hnc
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ ¬(m = 0 ∧ n = 0)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsWeaklyRegular M as ∧ Nontrivial (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ Nontrivial (M₂ ⧸ Ideal.ofList bs • ⊤)

Tactic:
let e' := QuotientAddGroup.congr _ _ e <|
    AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective h

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
e' : M ⧸ (Ideal.ofList as • ⊤).toAddSubgroup ≃+ M₂ ⧸ (Ideal.ofList bs • ⊤).toAddSubgroup :=
  QuotientAddGroup.congr (Ideal.ofList as • ⊤).toAddSubgroup (Ideal.ofList bs • ⊤).toAddSubgroup e ⋯
⊢ IsWeaklyRegular M as ∧ Nontrivial (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ Nontrivial (M₂ ⧸ Ideal.ofList bs • ⊤)
Module: Mathlib.RingTheory.DividedPowers.Padic

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

Tactic:
rw [← zpow_neg_one, ← zpow_zero ↑p]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ ⋃ i, ↑(J i), hI.dpow n s ∈ span (⋃ i, ↑(J i))

Tactic:
Set.mem_iUnion

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ ∀ {n : ℕ}, n ≠ 0 → ∀ (s : A), (∃ i, s ∈ ↑(J i)) → hI.dpow n s ∈ span (⋃ i, ↑(J i))
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ b ^ m * hI.dpow m a ∈ J * I

Tactic:
exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm))
        (hI.dpow_mem hm ha)

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ {r | r ∈ rs} = {r | r ∈ rs'}

Tactic:
exact Set.ext fun _ => h2.mem_iff

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 hI.SubDPIdeal
| ⨆ a ∈ S, ⟨a.carrier, ⋯⟩

Tactic:
iSup

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
| sSup (Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ Set.Finite.toFinset ⋯, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset ⋯
h2 : (s a).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Tactic:
Set.mem_iUnion

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ Set.Finite.toFinset ⋯, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ Set.Finite.toFinset ⋯
h2 : (s a).coeff g ≠ 0
⊢ ∃ i, g ∈ (s i).support
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos.refine_2
Γ : 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
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ ((PowerSeries.coeff i.snd.1) a * (PowerSeries.coeff i.snd.2) b) • (x ^ i.fst).coeff g = 0

Tactic:
mul_comm ((PowerSeries.coeff i.snd.1) a),

Goal state after:
case pos.refine_2
Γ : 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
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ ((PowerSeries.coeff i.snd.2) b * (PowerSeries.coeff i.snd.1) a) • (x ^ i.fst).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
by_cases hd₀ : d 0 = 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : ¬d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
rw [PowerSeries.subst, subst_comp_subst_apply _ hf.const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![PowerSeries.X, 0] s)) F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.FormalGroup.Basic

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

Tactic:
rw [PowerSeries.subst, subst_comp_subst_apply _ hf.const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![0, PowerSeries.X] s)) F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ HasSubst ![0, PowerSeries.X]
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
⊢ (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr.symm
      (ofLex a).orderTop =
    (ofLex (f₃ a)).orderTop

Tactic:
simp [f₃, ← OrderIso.withTopCongr_symm]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ #↑((single a) r).support = 1

Tactic:
support_single_of_ne h,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ #↑{a} = 1
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')⁻¹ʳ
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ ≡ a₀ [SMOD I]

Tactic:
sub_eq_add_neg,

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')⁻¹ʳ
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ c n + -(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ) ≡ a₀ [SMOD I]