mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) 0

Tactic:
indToCoindAux_of_not_rel,

Goal state after:
case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ 0 = (A.ρ s) 0

case inr.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ ¬(QuotientGroup.rightRel S) (↑s * g₁) g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

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

Tactic:
simp [d_eq, -LinearEquiv.toModuleIso_hom, -LinearEquiv.toModuleIso_inv]

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) ≫ (diagonalSuccIsoFree k G m).inv = 0

Tactic:
rw [Category.assoc, d_comp_diagonalSuccIsoFree_inv_eq, ← Category.assoc,
        d_comp_diagonalSuccIsoFree_inv_eq, Category.assoc, HomologicalComplex.d_comp_d,
        Limits.comp_zero]

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

Goal state before:
pp: case refine_2
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      (A.coinvariantsTensorFreeLEquiv (Fin i → G)).toModuleIso.symm.hom ≫
          (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d i j =
        (inhomogeneousChains A).d i j ≫ (A.coinvariantsTensorFreeLEquiv (Fin j → G)).toModuleIso.symm.hom

Tactic:
rintro i j rfl

Goal state after:
case refine_2
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
j : ℕ
⊢ (A.coinvariantsTensorFreeLEquiv (Fin (j + 1) → G)).toModuleIso.symm.hom ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (j + 1) j =
    (inhomogeneousChains A).d (j + 1) j ≫ (A.coinvariantsTensorFreeLEquiv (Fin j → G)).toModuleIso.symm.hom
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: case refine_2
k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
j : ℕ
⊢ (A.coinvariantsTensorFreeLEquiv (Fin (j + 1) → G)).toModuleIso.symm.hom ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (j + 1) j =
    (inhomogeneousChains A).d (j + 1) j ≫ (A.coinvariantsTensorFreeLEquiv (Fin j → G)).toModuleIso.symm.hom

Tactic:
simp [d_eq, -LinearEquiv.toModuleIso_hom, -LinearEquiv.toModuleIso_inv]

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
f : ↥(cocycles₂ A)
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, g⁻¹ * g)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g]
    at this

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
this : f (1, 1) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, 1)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) = 0

Tactic:
by ext g; simp [cochainsIso₀, x.2 (g 0),
      inhomogeneousCochains.d, Pi.zero_apply (M := fun _ => A)]

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

Goal state before:
pp: case h.refine_3
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π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
⊢ (fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) ∈ cocycles₁ (A.quotientToInvariants S)

Tactic:
rw [mem_cocycles₁_iff]
    intro g h
    induction g using QuotientGroup.induction_on with | @H g =>
    induction h using QuotientGroup.induction_on with | @H h =>
    apply Subtype.ext
    simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
⊢ (evalAlgHom k (fun a ↦ k) s) ((leftRegular t⁻¹) (single u 1)) = (rightRegular s) ((basisFun k G) u) t

Tactic:
by_cases u = t * s

Goal state after:
case pos
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
h✝ : u = t * s
⊢ (evalAlgHom k (fun a ↦ k) s) ((leftRegular t⁻¹) (single u 1)) = (rightRegular s) ((basisFun k G) u) t

case neg
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
h✝ : ¬u = t * s
⊢ (evalAlgHom k (fun a ↦ k) s) ((leftRegular t⁻¹) (single u 1)) = (rightRegular s) ((basisFun k G) u) t
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hP : (rename f) ↑P = ↑((MvPolynomial.rename f) P)
hQ : (rename f) ↑Q = ↑((MvPolynomial.rename f) Q)
⊢ (rename f) ↑(P + Q) = ↑((MvPolynomial.rename f) (P + Q))

Tactic:
| add P Q hP hQ =>

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
inst✝ : A.IsTrivial
⊢ (ModuleCat.Hom.hom 0).ker = ⊤

Tactic:
ModuleCat.hom_zero,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ LinearMap.ker 0 = ⊤
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (1, h) ((A.ρ g⁻¹) a) - single (g, 1) a ∈ boundaries₂ A

Tactic:
by
  use single (g, 1, h) a
  simp [d₃₂]

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
inst✝ : A.IsTrivial
⊢ (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv)
            (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) =
    (fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
      (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv) LinearMap.id.toAddMonoidHom).comp
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))

Tactic:
by
        ext
        simp only [H1ToTensorOfIsTrivial, Iso.toLinearEquiv, AddMonoidHom.coe_comp,
          LinearMap.toAddMonoidHom_coe, LinearMap.coe_comp, AddMonoidHom.coe_toIntLinearMap]
        -- todo: change this proof so that we don't need `change` and `simpa` that both abuse defeq.
        change TensorProduct.lift _ (QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _)) = _
        simpa [AddSubgroup.subtype, -π_comp_H1Iso_inv_apply, QuotientAddGroup.mk',
          cycles₁IsoOfIsTrivial_inv_apply (A := A)] using! (π_comp_H1Iso_inv_apply A _).symm

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)

Tactic:
rintro a ⟨x, _hx, b, hb, rfl⟩

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ ↑(I ^ n)
b : R
hb : b ∈ ↑(I ^ n)
⊢ (fun x1 x2 ↦ x1 * x2) x b ∈ ↑(I ^ n)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ↑(⊥ ^ 1) ⊆ U

Tactic:
simp [mem_of_mem_nhds U_nhds]

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
⊢ chainsMap f 0 = 0

Tactic:
ext; simp [chainsMap_f, LinearMap.zero_apply (M₂ := B)]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤
    (((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) ↑i • LinearMap.id) ∘ₗ
        ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ↥s).symm).range

Tactic:
lsum_smul_comp_finsuppLEquivDirectSum_symm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤
    ((map I ((lsum R) fun i ↦ ↑i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ↥s).symm) ∘ₗ
        ↑(sumEquivOfFintype I fun x ↦ M)).range
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 : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
⊢ (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)

Tactic:
have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)

Goal state after:
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))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
h' :
  (ConcreteCategory.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₂ ≫ (shortComplexH1 (A.toCoinvariants S)).g))
      Y =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₃)) Y
⊢ (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h.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.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
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
let b : G →₀ A := (x.1 : G →₀ A) + d₂₁ A W - lmapDomain _ k S.subtype Z

Goal state after:
case h.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.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
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
h1 : p.coeff x✝ ≠ 0
h2 : 1 ≤ (v.intAdicAbv hb) (p.coeff x✝)
⊢ x✝ ∈ p.support

Tactic:
simp [h1]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ (AddEquiv.toMultiplicative (Int.quotientZMultiplesNatEquivZMod n)).toMonoidHom
      ((QuotientGroup.map (powMonoidHom n).range (AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))
          v.valuationOfNeZero ⋯)
        ((QuotientGroup.mk' (powMonoidHom n).range) ((Units.map ↑(algebraMap R K)) x))) =
    1

Tactic:
QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ (AddEquiv.toMultiplicative (Int.quotientZMultiplesNatEquivZMod n)).toMonoidHom
      ↑(v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x)) =
    1
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : Ideal R
inst✝ : p.IsPrime
ass : p ∈ associatedPrimes R M
⊢ Ideal.comap (algebraMap R (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p)) ∈ associatedPrimes R M

Tactic:
simpa [Localization.AtPrime.under_maximalIdeal] using ass

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

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

Tactic:
by
  rcases ass with ⟨hp, x, hx⟩
  rcases fg with ⟨T, hT⟩
  rcases IsLocalizedModule.mk'_surjective S f x with ⟨⟨m, s⟩, rfl⟩
  simp only [Function.uncurry_apply_pair] at hx
  have mem (a : T) : algebraMap R R' a ∈ p := by
    simpa [← Ideal.mem_comap, ← hT] using Ideal.subset_span a.2
  simp only [hx, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, ← map_pow, algebraMap_smul,
    ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_eq_zero' f] at mem
  choose e g hg using mem
  refine ⟨.under R p, (∏ a, g a).1 • m, le_antisymm ?_ fun r hr ↦ ?_⟩
  · rw [← hT, Ideal.span_le]
    intro a ha
    simp only [SetLike.mem_coe, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton]
    obtain ⟨u, hu⟩ : g ⟨a, ha⟩ ∣ (∏ a, g a) := by
      apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)
    use e ⟨a, ha⟩
    rw [hu, Submonoid.coe_mul, smul_smul, ← mul_assoc, mul_comm, ← smul_smul, mul_comm, ← smul_smul]
    exact smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)
  · simp only [Ideal.mem_radical_iff, mem_bot, mem_colon_singleton, smul_smul] at hr
    obtain ⟨k, hk⟩ := hr
    have mem : r ^ k * (∏ a, g a).1 ∈ Ideal.comap (algebraMap R R') p := by
      rw [hx]
      use 1
      simp_rw [pow_one, mem_colon_singleton, algebraMap_smul, ← IsLocalizedModule.mk'_smul,
        hk, IsLocalizedModule.mk'_zero, mem_bot]
    apply hp.mem_of_pow_mem k
    rw [← map_pow]
    exact ((hp.under R).mul_mem_iff_mem_or_mem.mp mem).resolve_right
      (Set.disjoint_left.mp ((IsLocalization.disjoint_under_iff S R' p).mpr hp.1) (∏ a, g a).2)

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)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
have : Subsingleton (N ⟶ M) := Ext.addEquiv₀.subsingleton_congr.mp (h_ext 0 n.zero_lt_succ)

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)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: 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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M as

Tactic:
isWeaklyRegular_iff_Fin

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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| ∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) as[i]
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ dp R n m ^ k = ↑(k • {n}).multinomial * dp R (k * n) m

Tactic:
rw [Multiset.multinomial_nsmul_singleton, ← Fin.prod_const, prod_dp]
  simp [Nat.multinomial]

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

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

Tactic:
isWeaklyRegular_iff_Fin

Goal state after:
case b
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) bs[i]
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
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 : ℕ
m : M
⊢ (lift hI g hg) (dp R n m) = hI.dpow n (g m)

Tactic:
by rw [lift, lift'_apply_dp]

Goal state after: