mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
x : leftRegular k G ⟶ A
hi : Even i
⊢ (ModuleCat.Hom.hom (A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i (i + 1))) x =
    (ModuleCat.Hom.hom
        (((resolution k g hg).complex.linearYonedaObj k A).d i (i + 1) ≫ A.leftRegularHomEquiv.toModuleIso.hom))
      x

Tactic:
have : ¬(Even (i + 1)) := Nat.even_add_one.not_left.mpr hi

Goal state after:
case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
x : leftRegular k G ⟶ A
hi : Even i
this : ¬Even (i + 1)
⊢ (ModuleCat.Hom.hom (A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i (i + 1))) x =
    (ModuleCat.Hom.hom
        (((resolution k g hg).complex.linearYonedaObj k A).d i (i + 1) ≫ A.leftRegularHomEquiv.toModuleIso.hom))
      x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = (∑ x, g ↑(f x) * g (x z)) * ↑(f g)

Tactic:
Finset.sum_mul,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = ∑ i, g ↑(f i) * g (i z) * ↑(f g)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ cechNerveTerminalFrom G ≅ classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)

Tactic:
refine NatIso.ofComponents (fun _ => Types.productIso _) fun _ => ?_
  ext : 2
  exact Matrix.ext fun _ _ => Pi.lift_π_apply (f := fun _ ↦ G) _ _ _

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
simp [hφψ]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
simp [hφψ]

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

Goal state before:
pp: case h
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B : Rep k G
f : G →* H
φ : res f A✝ ⟶ B
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx : (ConcreteCategory.hom (H1InfRes A S).f) ((ConcreteCategory.hom (H1π (A.quotientToInvariants S))) x) = 0
⊢ (ConcreteCategory.hom (H1π (A.quotientToInvariants S))) x = 0

Tactic:
| @h x =>

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

Goal state before:
pp: case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.ofNat a✝))).ShortExact

pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact

Tactic:
· exact ShortComplex.shortExact_of_iso (ShortComplex.mapNatIso _ (tateComplex.evalNonneg _).symm)
      <| map_cochainsFunctor_eval_shortExact hS _

Goal state after:
case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
S : ShortComplex (Rep R G)
hS : S.ShortExact
a✝ : ℕ
⊢ (S.map
      (tateComplexFunctor R G ⋙ HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc a✝))).ShortExact
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx : (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
| @h x =>

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ (quotientToInvariantsFunctor k S ⋙ functor k (G ⧸ S) n).map φ ≫
      map (QuotientGroup.mk' S) (ofHom (Y.ρ.quotientToInvariants_lift S)) n =
    map (QuotientGroup.mk' S) (ofHom (X.ρ.quotientToInvariants_lift S)) n ≫ (functor k G n).map φ

Tactic:
simp only [Functor.comp_map, functor_map, ← cancel_epi (groupCohomology.π _ n),
      HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
      ← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp]

Goal state after:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ HomologicalComplex.cyclesMap
        (cochainsMap ((MonoidHom.id (G ⧸ S)).comp (QuotientGroup.mk' S))
          (resMap (QuotientGroup.mk' S) ((quotientToInvariantsFunctor k S).map φ) ≫
            ofHom (Y.ρ.quotientToInvariants_lift S)))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of Y.ρ)) n =
    HomologicalComplex.cyclesMap
        (cochainsMap ((QuotientGroup.mk' S).comp (MonoidHom.id G))
          (resMap (MonoidHom.id G) (ofHom (X.ρ.quotientToInvariants_lift S)) ≫ φ))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains Y) n
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range

Tactic:
apply Submodule.span_eq_of_le

Goal state after:
case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) ⊆ ↑(ModuleCat.Hom.hom (d₁₀ A)).range

case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range ≤ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ ∀ x ∈ I, C (constantCoeff x) ∈ I

Tactic:
intro f

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
⊢ f ∈ I → C (constantCoeff f) ∈ I
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
⊢ I ≤ comap constantCoeff (Ideal.map constantCoeff (span T))

Tactic:
intro f

Goal state after:
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⟧
⊢ f ∈ I → f ∈ comap constantCoeff (Ideal.map constantCoeff (span T))
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
this : RingHomSurjective constantCoeff
S : Set R⟦X⟧
inst✝ : (Ideal.span S).IsPrime
hI : X ∉ Ideal.span S
hfg : (Ideal.span S).FG
hS : S.Finite
hScard : S.ncard = (generators (Ideal.map constantCoeff (Ideal.span S))).ncard
⊢ Submodule.FG (Ideal.map constantCoeff (Ideal.span S))

Tactic:
exact map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

Tactic:
I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
simp [hφψ]

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 : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑A
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
simp [hφψ]

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
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
have surj : Function.Surjective f := by
    intro m
    rcases Ideal.toCotangent_surjective _ m with ⟨m', hm'⟩
    rcases Submodule.Quotient.mk_surjective _ (m'.1.1 2) with ⟨l, hl⟩
    have lmem : (transitionMap _ R (Nat.le_succ 1)) (m'.1.1 2) = m'.1.1 1 := m'.1.2 (Nat.le_succ 1)
    simp only [smul_eq_mul, Nat.succ_eq_add_one, Nat.reduceAdd, transitionMap, Submodule.factorPow,
      Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, ← hl, mk_eq_mk, factor_mk, pow_one,
      (mem_maximalIdeal_iff_eval_one_eq_zero m'.1).mp m'.2, eq_zero_iff_mem, mul_top] at lmem
    use (maximalIdeal R).toCotangent ⟨l, lmem⟩
    simp only [mapCotangent_toCotangent, Algebra.ofId_apply, ← hm', toCotangent_eq, f]
    change (of (maximalIdeal R) R l) - m' ∈ _
    simp only [maximalIdeal_eq_map, ← Ideal.map_pow]
    rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
    simpa [pow_smul_top_eq_ker_eval (maximalIdeal R).fg_of_isNoetherianRing, eval, sub_eq_zero]
      using hl

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
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : MvPowerSeries σ R
⊢ toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝) = x✝

Tactic:
ext; simp [coeff_toAdicCompletionInv, coeff_toAdicCompletion_val_apply_out]

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

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : ↥(cycles₁ A)
hx : (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
| @h x =>

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

Goal state before:
pp: case h
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 : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
⊢ ∃ a, (ConcreteCategory.hom (H1CoresCoinf A S).g) a = (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x

Tactic:
| @h x =>

Goal state after:
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ * y✝)) (Star.star (x✝ * z✝))

Tactic:
star_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star (x✝ * z✝))
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P) ∨ q.contentIdeal ≤ RingHom.ker (Ideal.Quotient.mk P)

Tactic:
simpa only [← map_eq_bot_iff_le_ker, ← contentIdeal_map_eq_map_contentIdeal, Polynomial.map_mul,
    contentIdeal_eq_bot_iff, mul_eq_zero] using hpq

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

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx : (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
| @h x =>

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
obtain ⟨x, mem_ann, hx⟩ := subsingleton_linearMap_iff.mp this

Goal state after:
case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n

Tactic:
rw [mul_comm, hI.dpow_mul ha, mul_comm]

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

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

Tactic:
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

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

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

Tactic:
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ r :: rs = []

Tactic:
rw [isRegular_iff, ne_comm, ← lt_top_iff_ne_top, Ideal.ofList_cons,
      sup_smul, ideal_span_singleton_smul, isWeaklyRegular_cons_iff] at h

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ DividedPowers (Ideal.span {↑p})

Tactic:
classical
  refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_
  · rw [Ideal.map_span, Set.image_singleton, map_natCast]
    simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]
    exact Nat.Prime.ne_zero hp.elim
  · intro n x hx
    exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • ↑n ! • hI.dpow n x

Tactic:
← smul_assoc

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (TensorProduct.lmul' (ULift.{u₁, u_1} R)).Flat ↔ (TensorProduct.lmul' R).Flat

Tactic:
conv_rhs => rw [← RingHom.Flat.ulift_iff.{u₁, u₂}]

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R) =
    (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
        (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))
⊢ (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₁} R)).Flat

Tactic:
rw [heq]

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R) =
    (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
        (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))
⊢ ((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
        (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))).Flat
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ
      ↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.extendScalars.h1CotangentEquivOfSurjective ⋯) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S

Tactic:
h1CotangentEquivOfSurjective_toLinearMap,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ((P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv) ∘ₗ h1Cotangentι) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm =
    H1Cotangent.δ R P.Ring S

Tactic:
LinearEquiv.comp_toLinearMap_symm_eq,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv) ∘ₗ h1Cotangentι =
    H1Cotangent.δ R P.Ring S ∘ₗ ↑P.h1CotangentExtendScalarsEquiv