mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inr.inl
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
hj : x ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

Tactic:
simp [decompose_of_mem _ hj, of_eq_of_ne, *]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inr.inr
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h✝ : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
h : i ≠ j
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

Tactic:
simp [decompose_of_mem _ hj, of_eq_of_ne, *]

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
f : PowerSeries R
g : Γ
hg : g = 0
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g

Tactic:
simp only [hg, coeff_hsum]

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
f : PowerSeries R
g : Γ
hg : g = 0
⊢ ∑ᶠ (i : ℕ), ((powerSeriesFamily 0 f) i).coeff 0 = (PowerSeries.constantCoeff f • 1).coeff 0
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
d : ℕ
⊢ (rescale (-1)) ↑(invOneSubPow A d) = binomialSeries A (-↑d)

Tactic:
by
  ext n
  rw [coeff_rescale, binomialSeries_coeff, ← Int.cast_negOnePow_natCast, ← zsmul_eq_mul]
  cases d with
  | zero =>
    by_cases hn : n = 0 <;> simp [invOneSubPow, Ring.choose_zero_ite, hn]
  | succ d =>
    simp only [invOneSubPow, coeff_mk, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg,
      zsmul_eq_mul, mul_one]
    rw [show (-1 : ℤ) + -d = -(d + 1) by abel, Ring.choose_neg, Nat.choose_symm_add, Units.smul_def,
      show (d : ℤ) + 1 + n - 1 = d + n by lia, ← Nat.cast_add, Ring.choose_natCast]
    norm_cast

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

Goal state before:
pp: case inr.right.refine_2
Γ : 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
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ ∀ (b : ℕ), b ≠ 0 → ((binomialFamily x r) b).coeff 0 = 0

Tactic:
· intro b hb
        exact coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (powerSeriesFamily x (mk fun m ↦ if m = 1 then 1 else 0)).hsum = x

Tactic:
powerSeriesFamily,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (smulFamily (fun n ↦ (coeff n) (mk fun m ↦ if m = 1 then 1 else 0)) (powers x)).hsum = x
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 = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
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

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)

Tactic:
intro g hn

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
hn : g ∈ (x ^ n).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)
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 : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
simp [← single_zero_ratCast, ← single_zero_intCast, ← single_zero_natCast, Rat.cast_def]

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

Goal state before:
pp: 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 (?m.34 J prime) (R ⧸ I)) J).IsMaximal

Tactic:
by
      convert! IsLocalRing.maximalIdeal.isMaximal R
      rw [Ideal.minimalPrimes, Set.mem_ofPred] at hp
      have := prime.comap (Ideal.Quotient.mk I)
      exact hp.eq_of_le ⟨this, .trans (by simp) (Ideal.ker_le_comap _)⟩ (le_maximalIdeal this.1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype J) I

Tactic:
by
      simp [← Submodule.map_le_iff_le_comap, Ideal.mul_le_left]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ (∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n) → p.height ≤ n

Tactic:
rintro ⟨I, hp, hI⟩

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
I : Ideal R
hp : p ∈ I.minimalPrimes
hI : Submodule.spanRank I ≤ ↑n
⊢ p.height ≤ n
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
e : R[X] ⧸ Ideal.map (algebraMap R R[X]) p ≃+* (R ⧸ p)[X] := p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] := Ideal.map e (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P)
⊢ (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).IsMaximal

Tactic:
refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
e : R[X] ⧸ Ideal.map (algebraMap R R[X]) p ≃+* (R ⧸ p)[X] := p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] := Ideal.map e (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P)
⊢ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) ≤ P
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
e : R[X] ⧸ Ideal.map (algebraMap R R[X]) p ≃+* (R ⧸ p)[X] := p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] := Ideal.map e (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P)
⊢ (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = 1

Tactic:
have : (P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))).IsMaximal := by
    refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_
    rw [mk_ker, LiesOver.over (P := P) (p := p)]
    exact map_comap_le

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
e : R[X] ⧸ Ideal.map (algebraMap R R[X]) p ≃+* (R ⧸ p)[X] := p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] := Ideal.map e (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P)
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).IsMaximal
⊢ (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = 1
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
t : Finset (Submodule R M)
ht : t.inf id = N
ht' : ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical)
⊢ ∃ t,
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
obtain ⟨u, hut, hu, hu'⟩ := decomposition_erase_inf ht

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
t : Finset (Submodule R M)
ht : t.inf id = N
ht' : ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary
ht'' : (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical)
u : Finset (Submodule R M)
hut : u ⊆ t
hu : u.inf id = N
hu' : ∀ ⦃J : Submodule R M⦄, J ∈ u → ¬(u.erase J).inf id ≤ J
⊢ ∃ t,
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) ∧
          ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
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
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
hq' : Ideal.comap (algebraMap S (T i)) q'.asIdeal = q
⊢ g' * (algebraMap S (T i)) (f i) ^ n ∉ q'.asIdeal

Tactic:
Ideal.mul_unit_mem_iff_mem

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
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
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
hq' : Ideal.comap (algebraMap S (T i)) q'.asIdeal = q
⊢ g' ∉ q'.asIdeal

case refine_1.hy
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
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
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
hq' : Ideal.comap (algebraMap S (T i)) q'.asIdeal = q
⊢ IsUnit ((algebraMap S (T i)) (f i) ^ n)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
S : Submonoid R
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M n
⊢ HasInjectiveDimensionLE (M.localizedModule S) n

Tactic:
have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
  induction n generalizing M with
  | zero =>
    have injle : HasInjectiveDimensionLE M 0 := ‹_›
    simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
      at injle ⊢
    rw [← Module.injective_iff_injective_object] at injle ⊢
    exact Module.injective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)
  | succ n ih =>
    have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
    rcases ei.1 M with ⟨I, inj, f, monof⟩
    let T := ShortComplex.mk f (cokernel.π f) (cokernel.condition f)
    have T_exact : T.ShortExact := { exact := ShortComplex.exact_cokernel f }
    have T_exact' : Function.Exact (ConcreteCategory.hom T.f) (ConcreteCategory.hom T.g) :=
      (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mp T_exact.1
    have TS_exact' := IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
      (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ T_exact'
    let TS := T.map (ModuleCat.localizedModuleFunctor S)
    have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
    let _ := (T_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mpr ‹_›
    let _ : Injective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).injective_obj _
    exact (TS_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mp (ih T.X₃)

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
this :
  IsScalarTower (A ⧸ P)
    (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
    (B ⧸ Q)
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

Tactic:
obtain ⟨σ', hσ'⟩ := Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under (G ⧸ N.1.1) P
    (Q.under (FixedPoints.subalgebra A B N.1.1)) σ

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
this :
  IsScalarTower (A ⧸ P)
    (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
    (B ⧸ Q)
σ' :
  (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
      Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) ≃ₐ[A ⧸ P]
    ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸ Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q
hσ' :
  ∀
    (x :
      ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
        Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q),
    (algebraMap
          (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
            Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
          (B ⧸ Q))
        (σ' x) =
      σ
        ((algebraMap
            (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup) ⧸
              Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
            (B ⧸ Q))
          x)
⊢ Nonempty ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
⊢ (hasseDeriv R k) ((single n) x) = (single (n - ↑k)) (Ring.choose n k • x)

Tactic:
by
  rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) PowerSeries.X ^ s) = exp (-↑s)

Tactic:
valuation_X_pow

Goal state after:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ exp (-↑s) = exp (-↑s)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
⊢ ↑s ∉ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P)

Tactic:
comap_map_eq_self_of_isMaximal _ h₀.ne_top

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
⊢ ↑s ∉ P
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ i ≤ ↑a✝ ∧ i ≠ ↑a✝ ↔ a✝ ≠ ⟨i, hin⟩ ∧ i ≤ ↑a✝

Tactic:
and_comm,

Goal state after:
case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ i ≠ ↑a✝ ∧ i ≤ ↑a✝ ↔ a✝ ≠ ⟨i, hin⟩ ∧ i ≤ ↑a✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ (exp (-1) ^ (Valued.v x).log)⁻¹ = Valued.v x

Tactic:
← exp_zsmul,

Goal state after:
case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ (exp ((Valued.v x).log • -1))⁻¹ = Valued.v x
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t

Tactic:
simp at h3

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
| (coeff (p • 0)) ((expand p hp) φ)

Tactic:
coeff_expand_smul

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
| (coeff 0) φ
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun x ↦ ‖f x.1 * g x.2‖) * C a ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)

Tactic:
Finset.sup'_mul₀ this

Goal state after:
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1 * g i.2‖ * C a) ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = wittStructureRat p Φ n * (C (1 / ↑p ^ n) * C (↑p ^ n))

Tactic:
← C_mul,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = wittStructureRat p Φ n * C (1 / ↑p ^ n * ↑p ^ n)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * (C (⅟↑p ^ n) * C (↑p ^ n)) =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Tactic:
← C_mul,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n * ↑p ^ n) =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * (C (↑p ^ n) * C (⅟↑p ^ n))

Tactic:
← C_mul,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * C (↑p ^ n * ⅟↑p ^ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
x✝ : ℕ
⊢ (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm 1), ⋯⟩ = (coeffMonoidHom N p x✝) 1

Tactic:
simp_rw [coeffMonoidHom_mk, map_one]

Goal state after: