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

Goal state before:
pp: case succ
k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (Y.resolutionX i).ρ.coind₁.coind₁ι.comp (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))) -
      coind₁ResMap φ ((Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))

Tactic:
ih,

Goal state after:
case succ
k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (Y.resolutionX i).ρ.coind₁.coind₁ι.comp (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ - (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ = ↑0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
ZeroMemClass.coe_zero,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ - (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ = 0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
C : ↑(groupCohomology A n) → Prop
h : ∀ (x : ↑(cocycles A n)), C ((ConcreteCategory.hom (π A n)) x)
y : ↑(cocycles A n)
⊢ C ((ConcreteCategory.hom (π A n)) y)

Tactic:
exact h y

Goal state after:
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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
g : G
x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                  (((lift
                        (↑A →ₗ[k]
                          ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                        k H)
                      fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                (((lift
                      (↑A →ₗ[k]
                        ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                      k H)
                    fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                  ↑(MonoidAlgebra.coeffLinearEquiv k))) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝

Tactic:
simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff]
        using! Coinvariants.sub_mem_ker _ _

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ barComplex.d k G (m + 1) ≫ barComplex.d k G m = 0

Tactic:
by
    have key : (d k G (m + 1) ≫ d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0 := by
      rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]
    exact (cancel_mono (diagonalSuccIsoFree k G m).inv).mp (by simpa using key)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
C : ↑(groupHomology A n) → Prop
h : ∀ (x : ↑(cycles A n)), C ((ConcreteCategory.hom (π A n)) x)
y : ↑(cycles A n)
⊢ C ((ConcreteCategory.hom (π A n)) y)

Tactic:
exact h y

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ 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)

Tactic:
exact div_eq_div_iff_mul_eq_mul.2 this.symm

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ H1π A ≫ (H1IsoOfIsTrivial A).hom = (cocycles₁IsoOfIsTrivial A).hom

Tactic:
simp [H1IsoOfIsTrivial, H1π]

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 : ℕ
⊢ Hom.toModuleCatHom φ ≫ (shortComplexH1 B).f = (shortComplexH1 A).f ≫ cochainsMap₁ f φ

Tactic:
by
    ext x
    funext g
    simpa [shortComplexH1, d₀₁, cochainsMap₁] using (hom_comm_apply φ g x).symm

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

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

Tactic:
by
  symm
  apply Submodule.span_eq_of_le
  · rintro _ ⟨x, rfl⟩
    use single x.1⁻¹ x.2
    simp [d₁₀]
  · rintro x ⟨y, hy⟩
    induction y using Finsupp.induction generalizing x with
    | zero => simp [← hy]
    | single_add _ _ _ _ _ h =>
      simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)]
        using! Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (iCycles A 2))
      (cyclesMk 2 1 cyclesMk₂_eq._proof_1 ((ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) ⋯) =
    (ConcreteCategory.hom (iCycles A 2)) ((ConcreteCategory.hom (isoCycles₂ A).inv) x)

Tactic:
by
    rw [iCycles_mk]
    simp only [ChainComplex.of_X, isoCycles₂_inv_comp_iCycles_apply]
    rfl

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
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x

Tactic:
intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩

Goal state after:
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₂
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝¹ : (𝓝 0).IsCountablyGenerated
this✝ : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
this : ∀ (i : ℕ), ∃ N, ∀ (n : ℕ), N ≤ n → u n - L ∈ I ^ i
⊢ Filter.Tendsto u Filter.atTop (𝓝 L)

Tactic:
by
      simpa [(hI.hasBasis_nhds L).tendsto_right_iff, sub_eq_neg_add]

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

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
intro V hV

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
cons_injective2.eq_iff

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ cyclesMap (MonoidHom.id G) (𝟙 A) n = 𝟙 (cycles A n)

Tactic:
simp [cyclesMap]

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

Goal state before:
pp: case w
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 : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯ ∈ cycles₁ (res S.subtype A)

Tactic:
· have : v + d₂₁ _ ve ∈ cycles₁ A := Submodule.add_mem _
      (Submodule.sub_mem _ hxc <| d₂₁_apply_mem_cycles₁ _) (d₂₁_apply_mem_cycles₁ _)
    rw [mem_cycles₁_iff] at this ⊢
    rwa [← sum_comapDomain, ← sum_comapDomain (g := fun _ a => a)] at this <;>
    exact ⟨Set.mapsTo_preimage _ _, Set.injOn_of_injective Subtype.val_injective,
      fun x hx => ⟨⟨x, hS hx⟩, hx, rfl⟩⟩

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ ≤ (p * q).contentIdeal.radical

Tactic:
calc
    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M), N.mkQ (r • x) = 0 → N.mkQ x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N

Tactic:
N.mkQ_apply,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M), Submodule.Quotient.mk (r • x) = 0 → Submodule.Quotient.mk x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (x : M), Submodule.Quotient.mk (r • x) = 0 → Submodule.Quotient.mk x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N

Tactic:
Submodule.Quotient.mk_eq_zero

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
⊢ (if 0 = 0 ∧ n✝ = 0 then 1 else 0) =
    ∑ k ∈ antidiagonal n✝, (if 0 = 0 ∧ k.1 = 0 then 1 else 0) * if 0 = 0 ∧ k.2 = 0 then 1 else 0

Tactic:
simp only [true_and, mul_ite, mul_one, mul_zero]

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
⊢ (if n✝ = 0 then 1 else 0) = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0
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]
      exact not_and_of_not_right (m = 0) hn

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ ↑n ! * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : ↑n ! * hI.dpow n a = a ^ n
⊢ a ^ n * hI.dpow 1 a = a ^ (n + 1)
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: 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
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)

Tactic:
have zero2 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext (i + 1) (by omega))

Goal state after:
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
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
zero2 : IsZero (AddCommGrpCat.of (Ext N M (i + 1)))
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
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
r : R
rs : List R
| ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

Tactic:
conv =>

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| Subsingleton (M ⧸ Ideal.ofList (r :: rs) • ⊤)

case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| Subsingleton (QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
gk : AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N ⋯)
⊢ Subsingleton (Ext N M (i + 1))

Tactic:
have mono_gk : Mono gk := by
          simp only [smulShortComplex_f_eq_smul_id, g, gk] at mono_g ⊢
          exact (Ext.postcomp_smul_id_mono_iff (a ^ k) (i + 1)).mpr <|
            ((Ext.postcomp_smul_id_mono_iff a (i + 1)).mp mono_g).pow k

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
gk : AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N ⋯)
mono_gk : Mono gk
⊢ Subsingleton (Ext N M (i + 1))
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (Ideal.ofList (r :: l₁✝) • ⊤).toAddSubgroup = (Ideal.ofList (s :: l₂✝) • ⊤).toAddSubgroup

Tactic:
conv =>

Goal state after:
case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map f (AddSubgroup.map ((toAddMonoidEnd R M) r) ⊤ ⊔ (Ideal.ofList l₁✝ • ⊤).toAddSubgroup)

case a
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
h : ∀ (x : M), f (r • x) = s • f x
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
| AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map f (AddSubgroup.map ((toAddMonoidEnd R M) r) ⊤) ⊔
      AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
ih,

Goal state after:
case cons
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₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map f (AddSubgroup.map ((toAddMonoidEnd R M) r) ⊤) ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup