mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : S.FiniteIndex
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
⊢ (indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom = X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f

Tactic:
ext g1 x g2

Goal state after:
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
inst✝ : S.FiniteIndex
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
g1 : G
x : ↑X✝
g2 : G
⊢ ↑(((AlgebraTensorModule.curry
                ((Hom.hom ((indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom)).toLinearMap ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X✝.ρ)) ∘ₗ
              MonoidAlgebra.lsingle g1)
            1)
          x)
      g2 =
    ↑(((AlgebraTensorModule.curry
                ((Hom.hom (X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f)).toLinearMap ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X✝.ρ)) ∘ₗ
              MonoidAlgebra.lsingle g1)
            1)
          x)
      g2
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:
induction m with

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
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 0 (0 + 1)))
      ((ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z) =
    0

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₀₁_comp_inv]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv)) ↑z = 0
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
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1))) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₀₁_comp_inv]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom (d₀₁ X.X₂ ≫ (cochainsIso₁ X.X₂).inv)) y g
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span (m.leadingTerm '' B) ≤ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]
    intro p hp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B) ≤ span (m.leadingTerm '' B)

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]
    intro p hp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
⊢ (rename g) ((rename f) p) = (rename (g ∘ f)) p

Tactic:
by
  classical
  ext y; simp only [coeff_rename]
  rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]

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

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

Tactic:
simp [isAdicComplete_iff, IsHausdorff.congr_ringEquiv, IsPrecomplete.congr_ringEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ IsAdic J ↔ (∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
by
  constructor
  · intro H
    change _ = _ at H
    rw [H]
    let := J.adicTopology
    constructor
    · intro n
      exact (J.openAddSubgroup n).isOpen'
    · intro s hs
      simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs
  · rintro ⟨H₁, H₂⟩
    apply IsTopologicalAddGroup.ext
    · apply @IsTopologicalRing.to_topologicalAddGroup
    · apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
    · ext s
      let := Ideal.adic_basis J
      rw [J.hasBasis_nhds_zero_adic.mem_iff]
      constructor <;> intro H
      · rcases H₂ s H with ⟨n, h⟩
        exact ⟨n, trivial, h⟩
      · rcases H with ⟨n, -, hn⟩
        rw [mem_nhds_iff]
        exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) (optionFunLeft σ R (p * q))) =
    (coeff x) ((PowerSeries.coeff k) (optionFunLeft σ R p * optionFunLeft σ R q))

Tactic:
simp only [coeff_coeff_optionFunLeft, coeff_mul, PowerSeries.coeff_mul, map_sum, sum_sigma']

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∑ p_1 ∈ antidiagonal (optionElim k x), (coeff p_1.1) p * (coeff p_1.2) q =
    ∑ x ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x,
      (coeff (optionElim x.fst.1 x.snd.1)) p * (coeff (optionElim x.fst.2 x.snd.2)) q
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
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
have rkeq := rank_eq_of_equiv_equiv _
    (LinearEquiv.ofBijective f ⟨inj, surj⟩).toAddEquiv
    (residueField_map_bijective R) (fun r m ↦ by
      rcases IsLocalRing.residue_surjective r with ⟨s, rfl⟩
      exact map_smul f s m )

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

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
hf : constantCoeff f = 0
⊢ ∀ (s : σ), IsNilpotent (MvPowerSeries.constantCoeff ((PowerSeries.toMvPowerSeries s) f))

Tactic:
by simp_all [constantCoeff, toMvPowerSeries_apply]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ counit (f a) = 1

Tactic:
rw [CoalgHomClass.counit_comp_apply, ha.counit_eq_one]

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

Goal state before:
pp: 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.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
⊢ β ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : IsDedekindDomain A
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
x : ClassGroup A
⊢ ((extendedHom B C).comp (extendedHom A B)) x = (extendedHom A C) x

Tactic:
exact extendedHom_comp_apply A B C x

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : ∃ s, p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
obtain ⟨_, ha⟩ := this

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
w✝ : R
ha : p.coeff n = w✝ • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
⊢ (x ∈ Set.range fun x ↦ single x 1) → IsGroupLikeElem R x

Tactic:
by rintro ⟨g, rfl⟩; exact isGroupLikeElem_single_one _

Goal state after:
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
⊢ mapCycles₂ (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ

Tactic:
by
  rw [← cyclesMap'_comp, ← mapShortComplexH2_comp]

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

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := i, inv := v, val_inv := iv, inv_val := vi } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
⊢ ⊥.colon {x} = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker

Tactic:
simp [SetLike.ext_iff]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
⊢ P f

Tactic:
induction f using Quot.induction_on with | _ F

Goal state after:
case h
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial (ℕ × M) R
⊢ P (Quot.mk (⇑(ringCon R M).toSetoid) F)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ hI.dpow (n, r • m).1 (g (n, r • m).2) = r ^ n • hI.dpow (n, m).1 (g (n, m).2)

Tactic:
by
      dsimp only
      rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ (↑m !)⁻¹ʳ * (x + y) ^ m =
    ∑ 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:
inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ (x + y) ^ m =
    ↑m ! *
      ∑ 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.Padic

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

Tactic:
have hnorm : 0 < ‖(n ! : ℚ_[p])‖ := by
      simp only [norm_pos_iff, ne_eq, cast_eq_zero]
      exact factorial_ne_zero n

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ ^ m * ↑(m * k)!) = ↑(m.uniformBell k)

Tactic:
inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑k !)⁻¹ʳ ^ m * ↑(m * k)! = ↑m ! * ↑(m.uniformBell k)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

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

Tactic:
have aux : ((n !) : R) = (n ! : ℚ) • (1 : R) := by
    rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]

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

Goal state before:
pp: case inl
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
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ span (↑J ∪ ↑K)

Tactic:
exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
a✝ : TrivSqZeroExt.fst x = 0
⊢ ∃ x_1, TrivSqZeroExt.snd x = TrivSqZeroExt.fst x_1

Tactic:
exact ⟨.inl x.snd, rfl⟩

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
⊢ hI.IsSubDPIdeal (sSup ((fun J ↦ J.carrier) '' S))

Tactic:
have h : (⋃ (i : Ideal A) (_ : i ∈ (fun J ↦ J.carrier) '' S), ↑i) ⊆ (I : Set A) := by
        rintro a ⟨-, ⟨J, rfl⟩, haJ⟩
        rw [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at haJ
        obtain ⟨J', hJ'⟩ := (Set.mem_image _ _ _).mp haJ.1
        exact  J'.isSubideal  (hJ'.2 ▸ haJ.2)
      rw [sSup_eq_iSup, Submodule.iSup_eq_span', submodule_span_eq, span_isSubDPIdeal_iff h]
      rintro n hn x ⟨T, ⟨J, rfl⟩, ⟨J', ⟨⟨hJ', rfl⟩, h'⟩⟩⟩
      apply subset_span
      apply Set.mem_biUnion hJ'
      obtain ⟨K, hKS, rfl⟩ := hJ'
      exact K.dpow_mem _ hn x h'

Goal state after: