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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i

Tactic:
ext n ω
    simp only [Pi.smul_apply, Finset.sum_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h : (fun f ↦ (↑f.toContinuousLinearMap).toFun) f = (fun f ↦ (↑f.toContinuousLinearMap).toFun) g
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h : (fun f ↦ (↑f.toContinuousLinearMap).toFun) f = (fun f ↦ (↑f.toContinuousLinearMap).toFun) g
x : V
⊢ f.toContinuousLinearMap x = g.toContinuousLinearMap x
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ f = default

Tactic:
ext x

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
⊢ (Hom.hom f) (y ⊗ₜ[k] (B.ρ g) x) = (C.ρ g) ((Hom.hom f) ((A.ρ g⁻¹) y ⊗ₜ[k] x))

Tactic:
have := by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
this : (C.ρ g) ((Hom.hom f) ((A.ρ g⁻¹) y ⊗ₜ[k] x)) = (Hom.hom f) (y ⊗ₜ[k] (B.ρ g) x)
⊢ (Hom.hom f) (y ⊗ₜ[k] (B.ρ g) x) = (C.ρ g) ((Hom.hom f) ((A.ρ g⁻¹) y ⊗ₜ[k] x))
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₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Tactic:
rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s, hs⟩ => ⟨s, by simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]⟩) h

Goal state after:
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
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
γ : G
this : x.coeff γ = x.coeff g
⊢ ((Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g))).coeff γ = x.coeff γ

Tactic:
simp [norm, Representation.norm, this]

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
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
⊢ ((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ A.ρ g =
    (MonoidHom.comp B.ρ φ) g ∘ₗ (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1

Tactic:
ext x

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
x : ↑A
⊢ (((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ A.ρ g) x =
    ((MonoidHom.comp B.ρ φ) g ∘ₗ (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
by
    have hxinv : Algebra.norm K x⁻¹ = 1 := by simp [Algebra.norm_inv, hx]
    obtain ⟨y, hy⟩ := H _ hxinv
    use y
    rw [IsUnit.div_eq_iff y.isUnit] at hy
    rw [hy]
    field_simp

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
⊢ (ModuleCat.Hom.hom (d₀₁ A)).ker = A.ρ.invariants

Tactic:
ext x

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k ↑A)
⊢ x ∈ (ModuleCat.Hom.hom (d₀₁ A)).ker ↔ x ∈ A.ρ.invariants
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 : G →* H
φ : res f A ⟶ B
ψ : res g A ⟶ B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap g ψ

Tactic:
subst hfg

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap f ψ
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 : G →* H
φ : res f A ⟶ B
ψ : res g A ⟶ B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
n : ℕ
⊢ map f φ n = map g ψ n

Tactic:
subst hfg

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
ψ : res f A ⟶ B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n
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
⊢ (cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom = (cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
ext x

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x : Fin 0 → H
x✝ : ↑A
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom) ∘ₗ LinearMap.single k (fun i ↦ ↑A) x) x✝ =
    (ModuleCat.Hom.hom ((cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ) ∘ₗ LinearMap.single k (fun i ↦ ↑A) x) x✝
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:
ext x

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : ↑(shortComplexH1 A).X₁
⊢ (ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1 B).f)) x =
    (ModuleCat.Hom.hom ((shortComplexH1 A).f ≫ cochainsMap₁ f φ)) x
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 : ℕ
⊢ cochainsMap₁ f φ ≫ (shortComplexH1 B).g = (shortComplexH1 A).g ≫ cochainsMap₂ f φ

Tactic:
ext x

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : ↑(shortComplexH1 A).X₂
⊢ (ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1 B).g)) x =
    (ModuleCat.Hom.hom ((shortComplexH1 A).g ≫ cochainsMap₂ f φ)) x
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
⊢ InducedCategory.homMk (↟(X.ρ g)) ≫ InducedCategory.homMk (↟(X.ρ g⁻¹)) = 𝟙 X.V

Tactic:
ext x

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
x : ↑X.V.obj
⊢ (Hom.hom (InducedCategory.homMk (↟(X.ρ g)) ≫ InducedCategory.homMk (↟(X.ρ g⁻¹))).hom) x = (Hom.hom (𝟙 X.V).hom) x
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
⊢ InducedCategory.homMk (↟(X.ρ g⁻¹)) ≫ InducedCategory.homMk (↟(X.ρ g)) = 𝟙 X.V

Tactic:
ext x

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
x : ↑X.V.obj
⊢ (Hom.hom (InducedCategory.homMk (↟(X.ρ g⁻¹)) ≫ InducedCategory.homMk (↟(X.ρ g))).hom) x = (Hom.hom (𝟙 X.V).hom) x
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 : ℕ
⊢ cochainsMap₁ f φ ≫ (shortComplexH2 B).f = (shortComplexH2 A).f ≫ cochainsMap₂ f φ

Tactic:
ext x

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : ↑(shortComplexH2 A).X₁
⊢ (ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f)) x =
    (ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ)) x
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 : ℕ
⊢ cochainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ cochainsMap₃ f φ

Tactic:
ext x

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n : ℕ
x : ↑(shortComplexH2 A).X₂
⊢ (ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g)) x =
    (ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ)) x
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ True

Tactic:
and_true,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, coeff xi x = 0 ∨ si ≤ xi
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
c : σ →₀ ℕ
hx : c + single i 1 ∈ ⇑degree ⁻¹' Set.Ici 1
hi : i ∈ (c + single i 1).support
⊢ c + single i 1 ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(Submodule.restrictScalars R (idealOfVars σ R))

Tactic:
simpa [monomial_add_single] using Ideal.mul_mem_left _ _ (Ideal.subset_span (by simp))

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ idealOfVars σ R ^ n = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯

Tactic:
rw [idealOfVars_eq_restrictSupportIdeal]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n = restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
⊢ renameFun f (p * q) = renameFun f p * renameFun f q

Tactic:
ext x

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ (coeff x) (renameFun f (p * q)) = (coeff x) (renameFun f p * renameFun f q)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
x : σ →₀ ℕ
⊢ (coeff x) a₁✝ = (coeff x) a₂✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ sSup C ∈ kaplanskySet S

Tactic:
rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∀ (x : R), x ∉ ↑(sSup C) ∩ ↑S
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 (g, 1) ((A.ρ g) a) - single (1, h) a ∈ boundaries₂ A

Tactic:
use single (g, 1, h) (A.ρ g (-a))

Goal state after:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₃₂ A)) (single (g, 1, h) ((A.ρ g) (-a))) = single (g, 1) ((A.ρ g) a) - single (1, h) a
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = ∑ᶠ (d : σ →₀ ℕ), (coeff d) p • (coeff n) (d.prod fun s e ↦ (X ∘ f) s ^ e)

Tactic:
finsum_eq_sum _
    (coeff_subst_finite (HasSubst.X_comp _) p n)

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = ∑ i ∈ Set.Finite.toFinset ⋯, (coeff i) p • (coeff n) (i.prod fun s e ↦ (X ∘ f) s ^ e)
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
x✝¹ : ↥(cycles₁ A).toAddSubgroup
y : G →₀ ↑A
hy : y ∈ (cycles₁ A).toAddSubgroup
x✝ : ⟨y, hy⟩ ∈ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
z : ↑(shortComplexH1 A).X₁
hz : (shortComplexH1 A).moduleCatToCycles z = ⟨y, hy⟩
⊢ ((Finsupp.liftAddHom fun g ↦
            ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
        (cycles₁ A).toAddSubgroup.subtype)
      ⟨y, hy⟩ =
    0

Tactic:
by
      simp [← hz, d₂₁, sum_sum_index, sum_add_index', tmul_add, sum_sub_index, tmul_sub,
        shortComplexH1]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤

Tactic:
suffices ∀ (a : R) (i : ℕ), ∃ j : ℕ, a • I ^ j ≤ I ^ i by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this
      intro r n
      use n
      rintro a ⟨x, hx, rfl⟩
      exact (I ^ n).smul_mem r hx

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
⊢ C ((↑↑constantCoeff).toFun x✝) = x✝

Tactic:
ext x

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ (coeff x) (C ((↑↑constantCoeff).toFun x✝)) = (coeff x) x✝
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
e : R ≃+* S
h : Ideal.map e.toRingHom i = i
⊢ Ideal.map e.toRingHom i ≤ i

Tactic:
by rw [h]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((optionEquivLeft (Fin n) R) ((rename ⇑(_root_.finSuccEquiv n)) p))) =
    (coeff (Finsupp.cons k x)) p

Tactic:
simp_rw [← Equiv.coe_toEmbedding, coeff_coeff_optionEquivLeft, ← embDomain_finSuccEquiv_cons,
    coeff_embDomain_rename]

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 : G →* H
φ : A ⟶ res f B
ψ : A ⟶ res g B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap g ψ

Tactic:
subst hfg

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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ chainsMap f φ = chainsMap f ψ
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 : G →* H
φ : A ⟶ res f B
ψ : A ⟶ res g B
hfg : f = g
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
n : ℕ
⊢ map f φ n = map g ψ n

Tactic:
subst hfg

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 : ℕ
ψ : A ⟶ res f B
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ map f φ n = map f ψ n
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
⊢ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ

Tactic:
ext x

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
x : Fin 1 → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : H
⊢ ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom)) x✝) a✝ =
    ((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle x) ≫ (chainsIso₁ A).hom ≫ chainsMap₁ f φ)) x✝) a✝
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
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (↑x a) = 0

Tactic:
refine Quotient.induction_on _ (x.val a) fun z ↦ ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(I ^ b • ⊤)
z : ↥(I ^ b • ⊤)
⊢ (LinearMap.reduceModIdeal (I ^ a) (I ^ b • ⊤).subtype) (Submodule.Quotient.mk z) = 0
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
⊢ (factorPow I ⋯).comp (f n) = f m

Tactic:
ext x

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
⊢ ((factorPow I ⋯).comp (f n)) x = (f m) x
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
φ : A ⟶ res 1 B
⊢ mapCycles₁ 1 φ ≫ H1π B = 0

Tactic:
ext x

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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ (ModuleCat.Hom.hom (mapCycles₁ 1 φ ≫ H1π B)) x = (ModuleCat.Hom.hom 0) x
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
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : ι → R
⊢ ((lsum (AdicCompletion I R)) fun i ↦ (algebraMap R (AdicCompletion I R)) (f i) • LinearMap.id) ∘ₗ
      ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm =
    (map I ((lsum R) fun i ↦ f i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ι).symm) ∘ₗ
      ↑(sumEquivOfFintype I fun x ↦ M)

Tactic:
ext
  -- simp [-algebraMap_smul, algebraMap_apply, -smul_eq_mul]
  simp only [algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, LinearMap.coe_comp,
    coe_lsum, LinearMap.coe_smul, LinearMap.id_coe, LinearEquiv.coe_coe, Function.comp_apply,
    finsuppLEquivDirectSum_symm_lof, Pi.smul_apply, id_eq, smul_zero, sum_single_index, smul_eval,
    mapQ_eq_factor, factor_eq_factor, of_apply, mkQ_apply, Ideal.Quotient.mk_eq_mk, mk_apply_coe,
    sumEquivOfFintype_apply, sum_lof, map_mk, AdicCauchySequence.map_apply_coe, map_smul]
  rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
⊢ RingHom.ker (evalOneₐ I).toRingHom = Ideal.map (algebraMap R (AdicCompletion I R)) I

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
⊢ x ∈ RingHom.ker (evalOneₐ I).toRingHom ↔ x ∈ Ideal.map (algebraMap R (AdicCompletion I R)) I