mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
⊢ ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε

Tactic:
have I : ∀ᶠ n in atTop, (∑ i ∈ range n, ‖(X i - Y k i) ω‖) / n < δ :=
    (tendsto_order.1 (h'ω k)).2 δ hk

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
⊢ ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
X : Type u_5
inst✝⁷ : CommRing k
inst✝⁶ : Monoid G
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G V
τ : Representation k G W
υ : Representation k G X
f : ρ.IntertwiningMap τ
g : G
x : V
⊢ (τ g) (f x) - f x = ↑f ((ρ g) x) - ↑f x

Tactic:
by simpa using congr($((f.isIntertwining' g).symm) x)

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Injective V

Tactic:
← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff,

Goal state after:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Injective (equivalenceModuleMonoidAlgebra.functor.obj V)
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
symm

Goal state after:
case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ↑(Nat.card G) = ∑ g, V.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A = 0

Tactic:
ext ⟨x, hx⟩ g

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : x ∈ A.ρ.invariants
g : G
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A)) ⟨x, hx⟩ g = (ModuleCat.Hom.hom 0) ⟨x, hx⟩ g
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 : (A.ρ 1) (f (1, g)) + f (1, 1 * g) = f (1 * 1, g) + f (1, 1)
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [map_one, Module.End.one_apply, one_mul, add_right_inj, this]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : G × G →₀ ↑X.X₂
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
⊢ (Rep.Hom.hom X.f) ((ModuleCat.Hom.hom (d₁₀ X.X₁)) x) = (Rep.Hom.hom X.f) 0

Tactic:
by
  have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH1]

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

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ d₁₀ M ≫ Hom.toModuleCatHom M.norm = 0

Tactic:
ext
  simp [d₁₀_single M]

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

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ (ChainComplex.of.d (fun n ↦ ModuleCat.of R ((Fin n → G) →₀ ↑M)) (fun n ↦ inhomogeneousChains.d M n) 1 0 ≫
        (chainsIso₀ M).hom) ≫
      Hom.toModuleCatHom M.norm =
    0

Tactic:
simp [← comp_d₁₀_eq _]

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

Goal state before:
pp: case h.refine_3.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π (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
h : G ⧸ S
g : G
⊢ Quotient.liftOn' (↑g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
    ((A.quotientToInvariants S).ρ ↑g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
      Quotient.liftOn' (↑g) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

Tactic:
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.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_4
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
⊢ (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩) =
    (ConcreteCategory.hom (H1π A)) x

Tactic:
symm

Goal state after:
case h.refine_4
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
⊢ (ConcreteCategory.hom (H1π A)) x =
    (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1))
      ((ConcreteCategory.hom (H1π (A.quotientToInvariants S)))
        ⟨fun g ↦ Quotient.liftOn' g (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯, ⋯⟩)
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝ : G
f : ↑rightFDRep.V.obj
⊢ (Hom.hom (rightFDRep.ρ x✝ ≫ InducedCategory.homMk (↟(leftRegular s))).hom) f =
    (Hom.hom (InducedCategory.homMk (↟(leftRegular s)) ≫ rightFDRep.ρ x✝).hom) f

Tactic:
funext _

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
s x✝¹ : G
f : ↑rightFDRep.V.obj
x✝ : G
⊢ (Hom.hom (rightFDRep.ρ x✝¹ ≫ InducedCategory.homMk (↟(leftRegular s))).hom) f x✝ =
    (Hom.hom (InducedCategory.homMk (↟(leftRegular s)) ≫ rightFDRep.ρ x✝¹).hom) f x✝
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
k : Type u_3
inst✝ : Field k
B : Set (MvPolynomial σ k)
⊢ span (m.leadingTerm '' B) = span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

Tactic:
apply span_leadingTerm_eq_span_monomial₀

Goal state after:
σ : Type u_1
m : MonomialOrder σ
k : Type u_3
inst✝ : Field k
B : Set (MvPolynomial σ k)
⊢ ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 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
⊢ (ModuleCat.Hom.hom (d₁₀ A)).range = Coinvariants.ker A.ρ

Tactic:
symm

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ Coinvariants.ker A.ρ = (ModuleCat.Hom.hom (d₁₀ A)).range
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Function.support fun d ↦ (coeff d) p • (coeff n) (d.prod fun s e ↦ (X ∘ f) s ^ e)
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
hP : X ∉ P
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
· exact le_trans (spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime
      hP hfg).le (Nat.le_succ _)

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
x : AdicCompletion (maximalIdeal R) R
⊢ x ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ↔ ↑x 1 = 0

Tactic:
have : (AdicCompletion.eval (maximalIdeal R) R 1).ker =
    (maximalIdeal R) • (⊤ : Submodule R (AdicCompletion (maximalIdeal R) R)) := by
    simp [← pow_smul_top_eq_ker_eval (maximalIdeal R).fg_of_isNoetherianRing]
  rw [maximalIdeal_eq_map, ← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
  simp [← this, eval]

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)) ⋯
⊢ ∀ (m : (maximalIdeal R).Cotangent), f m = 0 → m = 0

Tactic:
intro m hm

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)) ⋯
m : (maximalIdeal R).Cotangent
hm : f m = 0
⊢ m = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (toAdicCompletion σ R) ↑p = (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p

Tactic:
symm

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
⊢ (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p = (toAdicCompletion σ R) ↑p
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ ((factorPow I ⋯).comp (f n)) x = (f m) x

Tactic:
symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
m n : ℕ
hle : m ≤ n
x : R
⊢ (f m) x = ((factorPow I ⋯).comp (f n)) x
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 : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
⊢ x ∈
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range

Tactic:
let Y : S →₀ A := X.sum fun g f =>
    mapRange.linearMap (A.ρ g⁻¹) (lmapDomain _ k (fun s => MulAut.conjNormal g⁻¹ s) f) - f

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
X : G →₀ ↥S →₀ ↑A
hX : mapRange ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) ⋯ X = x
Y : ↥S →₀ ↑A :=
  X.sum fun g f ↦ (mapRange.linearMap (A.ρ g⁻¹)) ((lmapDomain (↑A) k fun s ↦ (MulAut.conjNormal g⁻¹) s) f) - f
⊢ x ∈
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range
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:
simp only [H1CoresCoinf_X₂, H1CoresCoinf_X₃, LinearMap.mem_ker, H1CoresCoinf_g,
    H1π_comp_map_apply (QuotientGroup.mk' S)] at hx

Goal state after:
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.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range
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:
by
    rw [star_mul, star_mul]
    exact (h2.star hr).mul (h1.star hr)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

Tactic:
rw [contentIdeal_def, span_le]
  simp only [Set.subset_def, Finset.mem_coe, mem_coeffs_iff]
  rintro r ⟨n, _, rfl⟩
  simp [coeff_mul, _root_.sum_mem, Submodule.mul_mem_mul, coeff_mem_contentIdeal]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ mapDomainOfBialgHom (mapDomainBialgHom R f) = f

Tactic:
by
  ext g; refine single_left_injective (R := R) one_ne_zero ?_; simp [single_mapDomainOfBialgHom]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ 0 = ∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0

Tactic:
symm

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
h : ¬n✝ = 0
⊢ (∑ x ∈ antidiagonal n✝, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) = 0
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.support R ↑N = PrimeSpectrum.zeroLocus ↑I
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:
Module.support_eq_zeroLocus,

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 : PrimeSpectrum.zeroLocus ↑(Module.annihilator R ↑N) = PrimeSpectrum.zeroLocus ↑I
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
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
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
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = n + 1
i : ℕ
hi : i < n + 1
le_rad : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
⊢ Subsingleton (Ext N M i)

Tactic:
Module.support_eq_zeroLocus,

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
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
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = n + 1
i : ℕ
hi : i < n + 1
le_rad : PrimeSpectrum.zeroLocus ↑(Module.annihilator R ↑N) ⊆ PrimeSpectrum.zeroLocus ↑I
⊢ Subsingleton (Ext N M i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]

Goal state after:
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 : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
⊢ Module.support R (R ⧸ I) = PrimeSpectrum.zeroLocus ↑I

Tactic:
Module.support_eq_zeroLocus,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
⊢ PrimeSpectrum.zeroLocus ↑(Module.annihilator R (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I